diff options
| -rw-r--r-- | kernel/retroknowledge.ml | 1 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 1 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 1 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 2 |
4 files changed, 4 insertions, 1 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index b645e256f..8b451e2b8 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -57,6 +57,7 @@ type int31_field = | Int31TimesC | Int31Div21 | Int31Div + | Int31Diveucl | Int31AddMulDiv | Int31Compare | Int31Head0 diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 846f135e6..dde522e14 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -49,6 +49,7 @@ type int31_field = | Int31TimesC | Int31Div21 | Int31Div + | Int31Diveucl | Int31AddMulDiv | Int31Compare | Int31Head0 diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index a4db32144..e129823f4 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -285,6 +285,7 @@ PRINTED BY pr_r_int31_field | [ "int31" "timesc" ] -> [ Retroknowledge.Int31TimesC ] | [ "int31" "div21" ] -> [ Retroknowledge.Int31Div21 ] | [ "int31" "div" ] -> [ Retroknowledge.Int31Div ] +| [ "int31" "diveucl" ] -> [ Retroknowledge.Int31Diveucl ] | [ "int31" "addmuldiv" ] -> [ Retroknowledge.Int31AddMulDiv ] | [ "int31" "compare" ] -> [ Retroknowledge.Int31Compare ] | [ "int31" "head0" ] -> [ Retroknowledge.Int31Head0 ] diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 885cd0daf..e80f209eb 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -350,7 +350,7 @@ Register sub31carryc as int31 minuscarryc in "coq_int31" by True. Register mul31 as int31 times in "coq_int31" by True. Register mul31c as int31 timesc in "coq_int31" by True. Register div3121 as int31 div21 in "coq_int31" by True. -Register div31 as int31 div in "coq_int31" by True. +Register div31 as int31 diveucl in "coq_int31" by True. Register compare31 as int31 compare in "coq_int31" by True. Register addmuldiv31 as int31 addmuldiv in "coq_int31" by True. Register lor31 as int31 lor in "coq_int31" by True. |