From de4f0bb5975afa5440445cecaeb84e9d29ee5614 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 4 Dec 2023 09:52:00 +0100
Subject: [PATCH] wip

---
 src/coq_elpi_vernacular.ml         | 7 +++++--
 src/coq_elpi_vernacular.mli        | 2 +-
 src/coq_elpi_vernacular_syntax.mlg | 6 ++++++
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 5bfcb1e84..6d20d977c 100644
--- 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
index 7601baf11..770a69ef4 100644
--- 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
index 42c36ab81..2a16b93f1 100644
--- 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