diff options
| author | Vincent Laporte | 2018-09-10 13:20:39 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | 736842d4cde09c667837dee8a633ff98ecf6a820 (patch) | |
| tree | f1004d1f56eca42109bba0a0680527c217e15264 /vernac | |
| parent | 2ec78477c720ba3a5343b49f25cfa9c1639adbba (diff) | |
Register: simpler syntax
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
3 files changed, 9 insertions, 4 deletions
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 *) |