wip

LPCIC · Dec 4, 2023 · de4f0bb · de4f0bb
1 parent b51ce6b
commit de4f0bb
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 3 deletions.
diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
@@ -700,8 +700,11 @@ let in_exported_program : nature * qualified_name * string -> Libobject.obj =
     ~cache:cache_program
     ~subst:(Some subst_program)) with object_stage = Summary.Stage.Synterp }
 
-let export_command p =
-  let p_str = String.concat "." p in
+let export_command ?as_ p =
+  let p_str =
+    match as_ with
+    | None -> String.concat "." p
+    | Some p -> String.concat "." p in
   let nature = Coq_elpi_programs.Synterp.get_nature p in
   Lib.add_leaf (in_exported_program (nature,p,p_str))
 
diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli
@@ -69,4 +69,4 @@ val run_tactic : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Geni
 val run_in_tactic : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Geninterp.interp_sign -> unit Proofview.tactic
 
 (* move to synterp *)
-val export_command : qualified_name -> unit
+val export_command : ?as_:qualified_name -> qualified_name -> unit
diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg
@@ -348,6 +348,12 @@ VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([
      let () = ignore_unknown_attributes atts in  
      ()
   }
+| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) "As" qualified_name(q) ] => { Vernacextend.(VtSideff ([],VtNow)) } SYNTERP AS _ {
+     EV.export_command ~as_:(snd q) (snd p)
+  } -> {
+     let () = ignore_unknown_attributes atts in  
+     ()
+  }
 | #[ atts = any_attribute ] [ "Elpi" qualified_name(p) elpi_cmd_arg_list(args) ] SYNTERP AS syndata
    { 
      let () = ignore_unknown_attributes atts in