From 2ec78477c720ba3a5343b49f25cfa9c1639adbba Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 7 Sep 2018 17:34:11 +0200 Subject: Retroknowledge: use GlobRef.t instead of Constr.t as entry --- vernac/g_vernac.mlg | 6 ++++-- vernac/ppvernac.ml | 6 +++++- vernac/vernacentries.ml | 14 +++++++++----- vernac/vernacexpr.ml | 3 ++- 4 files changed, 20 insertions(+), 9 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 44c0159d1b..42d9239f36 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"; IDENT "int31"; 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..9a356bbaef 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" ++ str "int31" ++ pr_qualid n) ) | VernacComments l -> return ( diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e6b3721134..2b4dfd19a6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1950,14 +1950,18 @@ 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 f = Retroknowledge.(KInt31 (int31_field_of_string (Libnames.string_of_qualid n))) in + Global.register f gr (********************) (* 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 *) -- cgit v1.2.3 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