Fix Int63 -> Uint63

coq-itauto.opam

@@ -3,7 +3,7 @@ maintainer: "frederic.besson@inria.fr"
 homepage: "https://gitlab.inria.fr/fbesson/itauto"
 dev-repo: "git+https://gitlab.inria.fr/fbesson/itauto.git"
 authors: ["Frédéric Besson"]
-bug-reports: "frederic.besson@inria.fr"
+bug-reports: ["frederic.besson@inria.fr" "https://gitlab.inria.fr/fbesson/itauto/-/issues"]
 license: "MIT"
 synopsis: "Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq"
 description: """
@@ -15,12 +15,16 @@ itauto also provides an SMT-like tactic for propositional reasoning modulo the s
 both arithmetic and function symbols.
 """
 
-build: [make "-j%{jobs}%"]
+build: [
+  [make "-j%{jobs}%"]
+  [make "test"] {with-test}
+ ]
 install: [make "install"]
 depends: [
   "ocaml" {>= "4.9~"}
   "coq" {= "dev"}
   "ocamlbuild" {build}
+  "coq-mathcomp-zify" {with-test}
 ]
 depopts: [ "ocamlformat" {build} ]
 

src/cdcl.ml

@@ -2,6 +2,7 @@
 
 open Names
 open Constr
+  
 module P = ProverPatch
 
 let show_theory_time =

test-suite/arith.v

 Require Import Cdcl.Itauto.
 
-Require Import Int63 Bool  ZArith Lia.
+Require Import Uint63 Bool  ZArith Lia.
 
 Import Formula.
 Import HCons.

test-suite/refl_bool.v

@@ -12,7 +12,7 @@ Qed.
 #[local] Instance le_leb : Reflect.RProp2 le := Reflect.mkrProp2 _ _ le leb is_true_le.
 
 Require Import Cdcl.Itauto.
-Require Import Int63.
+Require Import Uint63.
 
 Lemma map : forall a b, Is_true (a <=? b) -> a <= b.
 Proof.