Fix phase separation for lib:qid syntax

src/rocq_elpi_vernacular.ml

@@ -864,3 +864,36 @@ let export_command ~atts:proof ?as_ p =
   let nature = Rocq_elpi_programs.Synterp.get_nature p in
   Lib.add_leaf (in_exported_program (proof,nature,p,q))
 
+let get_lib_ref ?loc qid =
+  let id = String.concat "." (snd qid) in
+  try Rocqlib.lib_ref id
+  with Rocqlib.NotFoundRef _ ->
+    CErrors.user_err ?loc
+      Pp.(str "Global reference not found: lib:" ++ str id
+          ++ str " (you may need to require some .v file with \
+                  `Register ... as " ++ str id ++ str ".`).")
+
+[%%if coq = "9.0" || coq = "9.1" || coq = "9.2" || coq = "9.3"]
+let lib_ref ?loc ~expl qid =
+  let ref = get_lib_ref qid in
+  let path = Nametab.path_of_global ref in
+  let f = Libnames.qualid_of_path ~loc:(fst qid) path in
+  if expl then CAst.make ?loc Constrexpr.(CAppExpl((f,None),[]))
+  else CAst.make ?loc Constrexpr.(CRef (f, None))
+[%%else]
+let libref_tag = GenConstr.create "elpi-libref"
+
+let lib_ref ?loc ~expl qid = CAst.make ?loc @@ Constrexpr.CGenarg (Raw (libref_tag, (expl,qid)))
+
+let intern_libref ?loc ist (expl,qid) =
+  let gr = get_lib_ref ?loc qid in
+  let c = DAst.make ?loc @@ Glob_term.GRef (gr, None) in
+  let info = { Genintern.passthrough_impls = not expl } in
+  c, info
+
+let () =
+  Genintern.register_intern_constr_gen libref_tag intern_libref
+
+let () =
+  Genintern.register_intern_pat_gen libref_tag intern_libref
+[%%endif]

src/rocq_elpi_vernacular.mli

@@ -70,3 +70,6 @@ val run_in_tactic : loc:Loc.t -> ?program:qualified_name -> Elpi.API.Ast.Loc.t *
 
 (* move to synterp *)
 val export_command : atts:proof option -> ?as_:qualified_name -> qualified_name -> unit
+
+(** [loc] is loc of the whole [lib:qid], then we also get the loc of just the [qid] part. *)
+val lib_ref : ?loc:Loc.t -> expl:bool -> (Loc.t * qualified_name) -> Constrexpr.constr_expr

src/rocq_elpi_vernacular_syntax.mlg

@@ -80,15 +80,6 @@ let warning_legacy_accumulate_gen =
 let warning_legacy_accumulate ?loc () = warning_legacy_accumulate_gen ?loc true
 let warning_legacy_accumulate2 ?loc () = warning_legacy_accumulate_gen ?loc false
 
-let lib_ref id =
-  let id = String.concat "." (snd id) in
-  try Rocqlib.lib_ref id
-  with Rocqlib.NotFoundRef _ ->
-    CErrors.user_err
-      Pp.(str "Global reference not found: lib:" ++ str id
-          ++ str " (you may need to require some .v file with \
-                  `Register ... as " ++ str id ++ str ".`).")
-
 [%%if coq = "9.0" || coq = "9.1"]
 let lookahead_lib_colon kwstate strm =
   match Gramlib.LStream.peek_nth kwstate 0 strm with
@@ -143,14 +134,9 @@ GRAMMAR EXTEND Gram
 
   term: LEVEL "0"
     [ [ lookahead_lib_colon;IDENT "lib"; ":"; id = qualified_name -> {
-          let ref = lib_ref id in
-          let path = Nametab.path_of_global ref in
-          CAst.make ~loc Constrexpr.(CRef (Libnames.qualid_of_path ~loc:(fst id) path,None)) }
+          Rocq_elpi_vernacular.lib_ref ~loc ~expl:false id }
       | lookahead_lib_colon;IDENT "lib"; ":"; "@"; id = qualified_name -> {
-          let ref = lib_ref id in
-          let path = Nametab.path_of_global ref in
-          let f = Libnames.qualid_of_path ~loc:(fst id) path in
-          CAst.make ~loc Constrexpr.(CAppExpl((f,None),[])) } ] ]
+          Rocq_elpi_vernacular.lib_ref ~loc ~expl:true id } ] ]
   ;
 END