Enable creating Db without initial code

README.md

@@ -175,8 +175,8 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   [elpi-command](elpi/elpi-command-template.elpi).
 - `Elpi Tactic <qname>` creates a tactic `<qname>` containing the preamble
   [elpi-tactic](elpi/elpi-tactic-template.elpi).
-- `Elpi Db <dbname> <code>` creates a Db (a program that is accumulated into
-  other programs). `<code>` is the initial contents of the Db, including the
+- `Elpi Db <dbname> [<code>]` creates a Db (a program that is accumulated into
+  other programs). The optional `<code>` is the initial contents of the Db, including the
   type declaration of its constituting predicates.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a

src/coq_elpi_vernacular.ml

@@ -456,14 +456,14 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc,
     P.init_program n init;
     set_current_program (snd n)
 
-  let create_db ~atts n ~init:(loc,s) =
+  let create_db ~atts n ?init () =
     let do_init =
       match atts with
       | 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
+    match do_init, init with false, _ | _, None -> () | true, Some (loc, s) ->
       let unit = P.unit_from_string ~elpi loc s in
       P.init_db n unit  
 
@@ -511,7 +511,7 @@ module type Common = sig
   val create_program : atts:bool option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
   val create_command : atts:bool option -> program_name -> unit
   val create_tactic : program_name -> unit
-  val create_db : atts:phase option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
+  val create_db : atts:phase option -> program_name -> ?init:(Elpi.API.Ast.Loc.t * string) -> unit -> unit
 
 end
 

src/coq_elpi_vernacular.mli

@@ -47,7 +47,7 @@ module type Common = sig
   val create_program : atts:bool option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
   val create_command : atts:bool option -> program_name -> unit
   val create_tactic : program_name -> unit
-  val create_db : atts:phase option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit
+  val create_db : atts:phase option -> program_name -> ?init:(Elpi.API.Ast.Loc.t * string) -> unit -> unit
 
 end
 

src/coq_elpi_vernacular_syntax.mlg

@@ -283,13 +283,13 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF
      EV.Synterp.create_tactic p
    } -> {
      EV.Interp.create_tactic p }
-| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] SYNTERP AS atts
+| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string_opt(s) ] SYNTERP AS atts
    { 
      let atts = validate_attributes synterp_attribute atts in
-     EV.Synterp.create_db ~atts d ~init:s;
+     EV.Synterp.create_db ~atts d ?init:s ();
      atts
    } -> {
-     EV.Interp.create_db ~atts d ~init:s }
+     EV.Interp.create_db ~atts d ?init:s () }
 
 | #[ atts = any_attribute ] [ "Elpi" "Typecheck" ] SYNTERP AS _ 
    {