Merge pull request #611 from rlepigre/br/fix-phases

Enforce correct database initialisation.

Changelog.md

@@ -4,6 +4,7 @@
 
 ### Commands
 - New `Elpi Accumulate dbname File filename` allows to accumulate a file int a db
+- `Elpi Db` now only creates (and initialises) a database for the specified phase
 
 ### API
 - New `coq.parse-attributes` support for the `attlabel` specification,

apps/NES/theories/NES.v

@@ -3,20 +3,21 @@ From elpi.apps.NES Extra Dependency "nes_interp.elpi" as nes_interp.
 
 From elpi Require Import elpi.
 
-#[synterp] Elpi Db NES.db lp:{{
+#[phase="both"] Elpi Db NES.db lp:{{
 
-pred open-ns o:string, o:list string.
-:name "open-ns:begin"
-open-ns _ _ :- fail.
+typeabbrev path (list string).
+
+:index (2)
+pred ns o:path, o:modpath.
 
 }}.
 
-#[phase="both"] Elpi Accumulate NES.db lp:{{
+#[synterp] Elpi Accumulate NES.db lp:{{
 
-typeabbrev path (list string).
+pred open-ns o:string, o:list string.
+:name "open-ns:begin"
+open-ns _ _ :- fail.
 
-:index (2)
-pred ns o:path, o:modpath.
 }}.
 
 Elpi Command NES.Status.

src/coq_elpi_vernacular.ml

@@ -463,10 +463,11 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc,
       | None -> same_phase Interp P.stage
       | Some phase -> same_phase phase P.stage in
     let elpi = P.ensure_initialized () in
-    P.declare_db n;
-    if do_init then
+    if do_init then begin
+      P.declare_db n;
       let unit = P.unit_from_string ~elpi loc s in
       P.init_db n unit  
+    end
 
   let load_command = P.load_command
   let load_tactic = P.load_tactic