diff --git a/Changelog.md b/Changelog.md index 1156b8961..492359aad 100644 --- a/Changelog.md +++ b/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, diff --git a/apps/NES/theories/NES.v b/apps/NES/theories/NES.v index 5d8937a22..1a4902c61 100644 --- a/apps/NES/theories/NES.v +++ b/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. diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index eb0143a62..4753669dd 100644 --- a/src/coq_elpi_vernacular.ml +++ b/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