diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Int31/Int31.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 5c1c5d794d..f1b02759c5 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 by True. -Register int31 as int31 type by True. +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 by True. -Register add31c as int31 plusc by True. -Register add31carryc as int31 pluscarryc by True. -Register sub31 as int31 minus by True. -Register sub31c as int31 minusc by True. -Register sub31carryc as int31 minuscarryc by True. -Register mul31 as int31 times by True. -Register mul31c as int31 timesc by True. -Register div3121 as int31 div21 by True. -Register div31 as int31 diveucl by True. -Register compare31 as int31 compare by True. -Register addmuldiv31 as int31 addmuldiv by True. -Register lor31 as int31 lor by True. -Register land31 as int31 land by True. -Register lxor31 as int31 lxor by True. +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 by True. -Register tail031 as int31 tail0 by True. +Register head031 as int31 head0. +Register tail031 as int31 tail0. |