Merge PR #8447: Cleaning in the retroknowledge

4 files changed, 25 insertions, 9 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 44c0159d1b..650b28ea67 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,8 +212,10 @@ GRAMMAR EXTEND Gram
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
-      | IDENT "Register"; IDENT "Inline"; id = identref ->
-          { VernacRegister(id, RegisterInline) }
+      | IDENT "Register"; g = global; "as"; quid = qualid ->
+          { VernacRegister(g, RegisterRetroknowledge quid) }
+      | IDENT "Register"; IDENT "Inline"; g = global ->
+          { VernacRegister(g, RegisterInline) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 63e9e4fe49..e15e57a003 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1161,7 +1161,11 @@ open Pputils
       | VernacRegister (id, RegisterInline) ->
         return (
           hov 2
-            (keyword "Register Inline" ++ spc() ++ pr_lident id)
+            (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+        )
+      | VernacRegister (id, RegisterRetroknowledge n) ->
+        return (
+          hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n)
         )
       | VernacComments l ->
         return (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6b3721134..28abd1e6ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1950,14 +1950,23 @@ let vernac_locate = function
   | LocateOther (s, qid) -> print_located_other s qid
   | LocateFile f -> locate_file f
 
-let vernac_register id r =
+let vernac_register qid r =
+  let gr = Smartlocate.global_with_alias qid in
  if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let kn = Constrintern.global_reference id.v in
-  if not (isConstRef kn) then
-    user_err Pp.(str "Register inline: a constant is expected");
   match r with
-  | RegisterInline -> Global.register_inline (destConstRef kn)
+  | RegisterInline ->
+    if not (isConstRef gr) then
+      user_err Pp.(str "Register inline: a constant is expected");
+    Global.register_inline (destConstRef gr)
+  | RegisterRetroknowledge n ->
+    let path, id = Libnames.repr_qualid n in
+    if DirPath.equal path Retroknowledge.int31_path
+    then
+      let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
+      Global.register f gr
+    else
+      user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path))
 
 (********************)
 (* Proof management *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 11b2a7d802..ea69ed59a3 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -278,6 +278,7 @@ type extend_name =
    It will be extended with primitive inductive types and operators *)
 type register_kind =
   | RegisterInline
+  | RegisterRetroknowledge of qualid
 
 type bullet = Proof_bullet.t
 [@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
@@ -438,7 +439,7 @@ type nonrec vernac_expr =
   | VernacPrint of printable
   | VernacSearch of searchable * Goal_select.t option * search_restriction
   | VernacLocate of locatable
-  | VernacRegister of lident * register_kind
+  | VernacRegister of qualid * register_kind
   | VernacComments of comment list
 
   (* Proof management *)