Replaced Int31 with Uint63

The modified files are - MEll.v - Mod_op.v - montgomery.v
thery · Sep 20, 2023 · f611fa4 · f611fa4
1 parent ae85b57
commit f611fa4
Show file tree

Hide file tree

Showing 3 changed files with 234 additions and 233 deletions.
diff --git a/src/Coqprime/num/MEll.v b/src/Coqprime/num/MEll.v
@@ -8,7 +8,7 @@
 
 
 Require Import ZArith Znumtheory Zpow_facts.
-Require Import Int31 ZEll montgomery.
+Require Import Uint63 ZEll montgomery.
 
 Set Implicit Arguments.
 
@@ -1225,4 +1225,4 @@ Time Eval vm_compute in (ell_test
   (- 169382514530949104195348226967375250000355478911252124)
   1045670343788723904542107880373576189650857982445904291
 ).
-*)
+*)
diff --git a/src/Coqprime/num/Mod_op.v b/src/Coqprime/num/Mod_op.v
@@ -10,7 +10,7 @@ Set Implicit Arguments.
 
 From Bignums Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv.
 From Bignums Require Import DoubleCyclic BigN.
-Require Import CyclicAxioms Cyclic31.
+Require Import CyclicAxioms Cyclic63.
 Require Import ZArith ZCAux.
 Import CyclicAxioms DoubleType DoubleBase.