From 736842d4cde09c667837dee8a633ff98ecf6a820 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 10 Sep 2018 13:20:39 +0200
Subject: Register: simpler syntax

---
 vernac/g_vernac.mlg     | 2 +-
 vernac/ppvernac.ml      | 2 +-
 vernac/vernacentries.ml | 9 +++++++--
 3 files changed, 9 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 42d9239f36..650b28ea67 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,7 +212,7 @@ 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"; g = global; "as"; IDENT "int31"; quid = qualid ->
+      | IDENT "Register"; g = global; "as"; quid = qualid ->
           { VernacRegister(g, RegisterRetroknowledge quid) }
       | IDENT "Register"; IDENT "Inline"; g = global ->
           { VernacRegister(g, RegisterInline) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 9a356bbaef..e15e57a003 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1165,7 +1165,7 @@ open Pputils
         )
       | VernacRegister (id, RegisterRetroknowledge n) ->
         return (
-          hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ str "int31" ++ pr_qualid n)
+          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 2b4dfd19a6..28abd1e6ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1960,8 +1960,13 @@ let vernac_register qid r =
       user_err Pp.(str "Register inline: a constant is expected");
     Global.register_inline (destConstRef gr)
   | RegisterRetroknowledge n ->
-    let f = Retroknowledge.(KInt31 (int31_field_of_string (Libnames.string_of_qualid n))) in
-    Global.register f gr
+    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 *)
-- 
cgit v1.2.3