diff options
| -rw-r--r-- | kernel/retroknowledge.ml | 2 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 38 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
6 files changed, 32 insertions, 23 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index c1a8820bf0..e51c25c06b 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -80,6 +80,8 @@ let int31_field_of_string = | "lxor" -> Int31Lxor | s -> CErrors.user_err Pp.(str "Registering unknown int31 operator " ++ str s) +let int31_path = DirPath.make [ Id.of_string "int31" ] + (* record representing all the flags of the internal state of the kernel *) type flags = {fastcomputation : bool} diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 1fc3cfb817..0a2ef5300e 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -47,6 +47,8 @@ type field = val int31_field_of_string : string -> int31_field +val int31_path : DirPath.t + (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries As per now, there is only the possibility of registering things diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index f1b02759c5..ca7d3ec074 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -45,8 +45,8 @@ Inductive int31 : Type := I31 : digits31 int31. (* spiwack: Registration of the type of integers, so that the matchs in the functions below perform dynamic decompilation (otherwise some segfault occur when they are applied to one non-closed term and one closed term). *) -Register digits as int31 bits. -Register int31 as int31 type. +Register digits as int31.bits. +Register int31 as int31.type. Declare Scope int31_scope. Declare ML Module "int31_syntax_plugin". @@ -345,21 +345,21 @@ Definition lor31 n m := phi_inv (Z.lor (phi n) (phi m)). Definition land31 n m := phi_inv (Z.land (phi n) (phi m)). Definition lxor31 n m := phi_inv (Z.lxor (phi n) (phi m)). -Register add31 as int31 plus. -Register add31c as int31 plusc. -Register add31carryc as int31 pluscarryc. -Register sub31 as int31 minus. -Register sub31c as int31 minusc. -Register sub31carryc as int31 minuscarryc. -Register mul31 as int31 times. -Register mul31c as int31 timesc. -Register div3121 as int31 div21. -Register div31 as int31 diveucl. -Register compare31 as int31 compare. -Register addmuldiv31 as int31 addmuldiv. -Register lor31 as int31 lor. -Register land31 as int31 land. -Register lxor31 as int31 lxor. +Register add31 as int31.plus. +Register add31c as int31.plusc. +Register add31carryc as int31.pluscarryc. +Register sub31 as int31.minus. +Register sub31c as int31.minusc. +Register sub31carryc as int31.minuscarryc. +Register mul31 as int31.times. +Register mul31c as int31.timesc. +Register div3121 as int31.div21. +Register div31 as int31.diveucl. +Register compare31 as int31.compare. +Register addmuldiv31 as int31.addmuldiv. +Register lor31 as int31.lor. +Register land31 as int31.land. +Register lxor31 as int31.lxor. Definition lnot31 n := lxor31 Tn n. Definition ldiff31 n m := land31 n (lnot31 m). @@ -485,5 +485,5 @@ Definition tail031 (i:int31) := end) i On. -Register head031 as int31 head0. -Register tail031 as int31 tail0. +Register head031 as int31.head0. +Register tail031 as int31.tail0. 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 *) |