Test asynchronous and make the selected lemmas persistant (#66)

* Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though)

* Make the selected lemmas persistant

Co-authored-by: Chantal Keller <Chantal.Keller@lri.fr>

4 files changed, 246 insertions, 202 deletions

diff --git a/unit-tests/Makefile b/unit-tests/Makefile
index d8e9be0..4820887 100644
--- a/unit-tests/Makefile
+++ b/unit-tests/Makefile
@@ -7,6 +7,7 @@ OBJ=$(ZCHAFFLOG) $(VERITLOG)
 COQLIBS?= -R ../src SMTCoq
 OPT?=
 COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+VIOFLAG?=-quick
 COQC?=$(COQBIN)coqc
 
 
@@ -39,9 +40,17 @@ logs: $(OBJ)
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
 
 
+%.vio: %.v logs
+	$(COQC) $(VIOFLAG) $(COQDEBUG) $(COQFLAGS) $*
+
+
+parallel: Tests_zchaff_tactics.vio Tests_verit_tactics.vio Tests_lfsc_tactics.vio
+	coqtop -schedule-vio-checking 3 Tests_zchaff_tactics Tests_verit_tactics Tests_lfsc_tactics
+
+
 clean: cleanvo
 	rm -rf *~ $(ZCHAFFLOG) $(VERITLOG)
 
 
 cleanvo:
-	rm -rf *~ *.vo *.glob
+	rm -rf *~ *.vo *.glob *.vio
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v
index ee9df76..2268cb9 100644
--- a/unit-tests/Tests_lfsc_tactics.v
+++ b/unit-tests/Tests_lfsc_tactics.v
@@ -29,7 +29,7 @@ Local Open Scope bv_scope.
   Goal forall (a b c: bitvector 4),
                                  (c = (bv_and a b)) ->
                                  ((bv_and (bv_and c a) b) = c).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -38,19 +38,19 @@ Local Open Scope bv_scope.
       bv2 = #b|1|0|0|0|  /\
       bv3 = #b|1|1|0|0|  ->
       bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3.
-  Proof. 
+  Proof using. 
      smt.
   Qed.
 
 
   Goal forall (a: bitvector 32), a = a.
-  Proof.
+  Proof using.
     smt.
   Qed.
 
   Goal forall (bv1 bv2: bitvector 4),
        bv1 = bv2 <-> bv2 = bv1.
-  Proof.
+  Proof using.
      smt.
   Qed.
 
@@ -64,7 +64,7 @@ Section Arrays.
 
 
   Goal forall (a:farray Z Z) i j, i = j -> a[i] = a[j].
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -74,7 +74,7 @@ Section Arrays.
          (f: Z -> Z),
          (a[x <- v] = b) /\ a[y <- w] = b  ->
          (f x) = (f y) \/  (g a) = (g b).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -85,7 +85,7 @@ Section Arrays.
   (*     d = b[0%Z <- 4][1%Z <- 4]  -> *)
   (*     a = d[1%Z <- b[1%Z]]  -> *)
   (*     a = c. *)
-  (* Proof. *)
+  (* Proof using. *)
   (*   smt. *)
   (* Qed. *)
 
@@ -93,7 +93,7 @@ Section Arrays.
 (*
   Goal forall (a b: farray Z Z) i,
       (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) =  4.
-  Proof.
+  Proof using.
     smt.
     rewrite read_over_other_write; try easy.
     rewrite read_over_same_write; try easy; try apply Z_compdec.
@@ -111,7 +111,7 @@ Section EUF.
          (x y: Z)
          (f: Z -> Z),
          y = x -> (f x) = (f y).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -119,7 +119,7 @@ Section EUF.
          (x y: Z)
          (f: Z -> Z),
          (f x) = (f y) -> (f y) = (f x).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -128,7 +128,7 @@ Section EUF.
          (x y: Z)
          (f: Z -> Z),
          x + 1 = (y + 1) -> (f y) = (f x).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -137,7 +137,7 @@ Section EUF.
          (x y: Z)
          (f: Z -> Z),
          x = (y + 1) -> (f y) = (f (x - 1)).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -145,7 +145,7 @@ Section EUF.
          (x y: Z)
          (f: Z -> Z),
          x = (y + 1) -> (f (y + 1)) = (f x).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -156,44 +156,44 @@ Section LIA.
 
 
   Goal forall (a b: Z), a = b <-> b = a.
-  Proof.
+  Proof using.
     smt.
   Qed.
 
   Goal forall (x y: Z), (x >= y) -> (y < x) \/ (x = y).
-  Proof. 
+  Proof using. 
     smt. 
   Qed.
 
 
   Goal forall (f : Z -> Z) (a:Z), ((f a) > 1) ->  ((f a) + 1) >= 2 \/((f a) = 30) .
-  Proof.
+  Proof using.
    smt.
   Qed.
  
   Goal forall x: Z, (x = 0%Z) -> (8 >= 0).
-  Proof.
+  Proof using.
     smt.
    Qed.
 
   Goal forall x: Z, ~ (x < 0%Z) -> (8 >= 0).
-  Proof. 
+  Proof using. 
     smt. 
   Qed.
 
   Goal forall (a b: Z), a < b -> a < (b + 1).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
   Goal forall (a b: Z), (a < b) -> (a + 2) < (b + 3).
-  Proof.
+  Proof using.
     smt.
   Qed.
 
 
   Goal forall a b, a < b -> a < (b + 10).
-  Proof. 
+  Proof using.
     smt.
   Qed.
 
@@ -208,141 +208,152 @@ Section PR.
 (* Simple connectors *)
 
 Goal forall (a:bool), a || negb a.
+Proof using.
   smt.
 Qed.
 
 Goal forall a, negb (a || negb a) = false.
+Proof using.
   smt.
 Qed.
 
 Goal forall a, (a && negb a) = false.
+Proof using.
   smt.
 Qed.
 
 Goal forall a, negb (a && negb a).
+Proof using.
   smt.
 Qed.
 
 Goal forall a, a --> a.
+Proof using.
   smt.
 Qed.
 
 Goal forall a, negb (a --> a) = false.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a , (xorb a a) || negb (xorb a a).
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a, (a||negb a) || negb (a||negb a).
+Proof using.
   smt.
 Qed.
 
 (* Polarities *)
 
 Goal forall a b, andb (orb (negb (negb a)) b) (negb (orb a b)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 (* Multiple negations *)
 
 Goal forall a, orb a (negb (negb (negb a))) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c,
   (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal true.
+Proof using.
   smt.
 Qed.
 
 Goal negb false.
+Proof using.
   smt.
 Qed.
 
  
 Goal forall a, Bool.eqb a a.
-Proof.
+Proof using.
   smt.
 Qed.
 
  
 Goal forall (a:bool), a = a.
+Proof using.
   smt.
 Qed.
 
 Goal (false || true) && false = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal negb true = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal false = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)).
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall x y, Bool.eqb (x --> y) ((x && y) || (negb x)).
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)).
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall a, ((a || a) && (negb a)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a, (negb (a || (negb a))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c,
   (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -353,19 +364,19 @@ Goal forall i j k,
   let b := j == k in
   let c := k == i in
   (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -458,35 +469,35 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42
   (orb (orb (orb x13 x23) x33) x43) &&
   (orb (orb (orb x14 x24) x34) x44) &&
   (orb (orb (orb x15 x25) x35) x45)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c f p, ((Z.eqb a c) && (Z.eqb b c) && ((negb (Z.eqb (f a) (f b))) || ((p a) && (negb (p b))))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall x y z f, ((Z.eqb x y) && (Z.eqb y z) && (negb (Z.eqb (f x) (f z)))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall x y z f, ((negb (Z.eqb (f x) (f y))) && (Z.eqb y z) && (Z.eqb (f x) (f (f z))) && (Z.eqb x y)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall a b c d e f, ((Z.eqb a b) && (Z.eqb b c) && (Z.eqb c d) && (Z.eqb c e) && (Z.eqb e f) && (negb (Z.eqb a f))) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -494,54 +505,54 @@ Qed.
 
 Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9))) -->
   ((x + y <=? 10) || (x + z <=? 12)) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall x, (Z.eqb (x - 3) 7)  -->  (x >=? 10) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall x y, (x >? y) --> (y + 1 <=? x) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall x y, ((x + y <=? - (3)) && (y >=? 0) 
         || (x <=? - (3))) && (x >=? 0) = false. 
- Proof. 
+ Proof using. 
    smt.
  Qed. 
 
 Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3))) --> (x >=? 10) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall x, (Z.eqb (x - 3) 7) --> (10 <=? x) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 (* More general examples *)
 Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 
 Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
   (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b).
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -551,7 +562,7 @@ Goal forall b1 b2 x1 x2,
     (ifb b2 (Z.eqb (2*x1+1) (2*x2+1)) (Z.eqb (2*x1+1) (2*x2)))
     (ifb b2 (Z.eqb (2*x1) (2*x2+1)) (Z.eqb (2*x1) (2*x2)))) -->
   ((b1 --> b2) && (b2 --> b1) && (Z.eqb x1 x2)).
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -560,14 +571,14 @@ Qed.
 Goal forall b,
   let a := b in
   a && (negb a) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall b,
   let a := b in
   a || (negb a) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -575,14 +586,14 @@ Qed.
 Goal forall i j,
   let a := i == j in
   a && (negb a) = false.
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall i j,
   let a := i == j in
   a || (negb a) = true.
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -590,19 +601,19 @@ Qed.
 (* Congruence in which some premises are REFL *)
 Goal forall (f:Z -> Z -> Z) x y z,
   (Z.eqb x y) --> (Z.eqb (f z x) (f z y)).
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall (f:Z -> Z -> Z) x y z,
   (x = y) -> (f z x) = (f z y).
-Proof.
+Proof using.
   smt.
 Qed.
 
 Goal forall (P:Z -> Z -> bool) x y z,
   (Z.eqb x y) --> ((P z x) --> (P z y)).
-Proof.
+Proof using.
   smt.
 Qed.
 
@@ -625,7 +636,7 @@ Section A_BV_EUF_LIA_PR.
   (*     d = b[bv1 <- 4][bv2 <- 4]  -> *)
   (*     a = d[bv2 <- b[bv2]]  -> *)
   (*     a = c. *)
-  (* Proof. *)
+  (* Proof using. *)
   (*   smt. *)
   (* Qed. *)
 
@@ -638,7 +649,7 @@ Section A_BV_EUF_LIA_PR.
   (*     d = b[bv1 <- 4][bv2 <- 4]  /\ *)
   (*     a = d[bv2 <- b[bv2]]  -> *)
   (*     a = c. *)
-  (* Proof. *)
+  (* Proof using. *)
   (*   smt. *)
   (* Qed. *)
 
@@ -652,7 +663,7 @@ Section A_BV_EUF_LIA_PR.
               r = s /\ h r = v /\ h s = y ->
               v < x + 1 /\ v > x - 1 ->
               f (h r) = f (h s) \/ g a = g b.
-  Proof.
+  Proof using.
     smt. (** "cvc4. verit." also solves the goal *)
   Qed.
 
@@ -666,7 +677,7 @@ Section A_BV_EUF_LIA_PR.
               a[z <- w] = b /\ a[t <- v] = b ->
               r = s -> v < x + 10 /\ v > x - 5 ->
               ~ (g a = g b) \/ f (h r) = f (h s).
-  Proof.
+  Proof using.
     smt. (** "cvc4. verit." also solves the goal *)
   Qed.
 
@@ -677,7 +688,7 @@ Section A_BV_EUF_LIA_PR.
       b[bv_add y x <- v] = a /\
       b = a[bv_add x y <- v]  ->
       a = b.
-  Proof.
+  Proof using.
     smt.
     (* CVC4 preprocessing hole on BV *)
     replace (bv_add x y) with (bv_add y x)
@@ -686,12 +697,12 @@ Section A_BV_EUF_LIA_PR.
   Qed.
 
   Goal forall (a:farray Z Z), a = a.
-  Proof.
+  Proof using.
     smt.
   Qed.
 
   Goal forall (a b: farray Z Z), a = b <->  b = a.
-  Proof.
+  Proof using.
     smt.
   Qed.
 
@@ -714,15 +725,15 @@ Section group.
 
   Lemma inverse' :
     forall a : Z, (op a (inv a) =? e).
-  Proof. smt. Qed.
+  Proof using associative identity inverse. smt. Qed.
 
   Lemma identity' :
     forall a : Z, (op a e =? a).
-  Proof. smt inverse'. Qed.
+  Proof using associative identity inverse. smt inverse'. Qed.
 
   Lemma unique_identity e':
     (forall z, op e' z =? z) -> e' =? e.
-  Proof. intros pe'; smt pe'. Qed.
+  Proof using associative identity inverse. intros pe'; smt pe'. Qed.
 
   Clear_lemmas.
 End group.
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 6ed1d67..6f0cb7e 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -23,14 +23,14 @@ Open Scope Z_scope.
 
 Lemma check_univ (x1: bool):
   (x1 && (negb x1)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 Lemma fun_const2 :
   forall f (g : Z -> Z -> bool),
     (forall x, g (f x) 2) -> g (f 3) 2.
-Proof.
+Proof using.
   intros f g Hf. verit Hf.
 Qed.
 
@@ -38,51 +38,62 @@ Qed.
 (* Simple connectives *)
 
 Goal forall (a:bool), a || negb a.
+Proof using.
   verit.
 Qed.
 
 Goal forall a, negb (a || negb a) = false.
+Proof using.
   verit.
 Qed.
 
 Goal forall a, (a && negb a) = false.
+Proof using.
   verit.
 Qed.
 
 Goal forall a, negb (a && negb a).
+Proof using.
   verit.
 Qed.
 
 Goal forall a, implb a a.
+Proof using.
   verit.
 Qed.
 
 Goal forall a, negb (implb a a) = false.
+Proof using.
   verit.
 Qed.
 
 Goal forall a , (xorb a a) || negb (xorb a a).
+Proof using.
   verit.
 Qed.
 
 Goal forall a, (a||negb a) || negb (a||negb a).
+Proof using.
   verit.
 Qed.
 
 Goal true.
+Proof using.
   verit.
 Qed.
 
 Goal negb false.
+Proof using.
   verit.
 Qed.
 
 Goal forall a, Bool.eqb a a.
-Proof.
+Proof using.
   verit.
 Qed.
 
 Goal forall (a:bool), a = a.
+Proof using.
   verit.
 Qed.
 
@@ -90,43 +101,43 @@ Qed.
 (* Other connectives *)
 
 Goal (false || true) && false = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal negb true = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal false = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)).
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal forall x y, Bool.eqb (negb (xorb x y)) ((x && y) || ((negb x) && (negb y))).
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)).
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)).
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -134,7 +145,7 @@ Qed.
 (* Multiple negations *)
 
 Goal forall a, orb a (negb (negb (negb a))) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -142,13 +153,13 @@ Qed.
 (* Polarities *)
 
 Goal forall a b, andb (orb a b) (negb (orb a b)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -157,7 +168,7 @@ Qed.
 (* ((a ∧ b) ∨ (b ∧ c)) ∧ ¬b = ⊥ *)
 
 Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -166,7 +177,7 @@ Qed.
 (* (a ∨ a) ∧ ¬a = ⊥ *)
 
 Goal forall a, ((a || a) && (negb a)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -175,7 +186,7 @@ Qed.
 (* ¬(a ∨ ¬a) = ⊥ *)
 
 Goal forall a, (negb (a || (negb a))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -185,7 +196,7 @@ Qed.
 
 Goal forall a b c,
     (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -197,7 +208,7 @@ Goal forall i j k,
     let b := j == k in
     let c := k == i in
     (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -206,7 +217,7 @@ Qed.
 (* (a ∧ b) ∧ (c ∨ d) ∧ ¬(c ∨ (a ∧ b ∧ d)) = ⊥ *)
 
 Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -215,7 +226,7 @@ Qed.
 (* a ∧ b ∧ c ∧ (¬a ∨ ¬b ∨ d) ∧ (¬d ∨ ¬c) = ⊥ *)
 
 Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -309,7 +320,7 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42
   (orb (orb (orb x13 x23) x33) x43) &&
   (orb (orb (orb x14 x24) x34) x44) &&
   (orb (orb (orb x15 x25) x35) x45)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -317,7 +328,7 @@ Qed.
 (* uf1.smt *)
 
 Goal forall a b c f p, ( (a =? c) && (b =? c) && ((negb (f a =?f b)) || ((p a) && (negb (p b))))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -325,7 +336,7 @@ Qed.
 (* uf2.smt *)
 
 Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -333,7 +344,7 @@ Qed.
 (* uf3.smt *)
 
 Goal forall x y z f, ((x =? y) && (y =? z) && (negb (f x =? f z))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -341,7 +352,7 @@ Qed.
 (* uf4.smt *)
 
 Goal forall x y z f, ((negb (f x =? f y)) && (y =? z) && (f x =? f (f z)) && (x =? y)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -349,7 +360,7 @@ Qed.
 (* uf5.smt *)
 
 Goal forall a b c d e f, ((a =? b) && (b =? c) && (c =? d) && (c =? e) && (e =? f) && (negb (a =? f))) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -358,28 +369,28 @@ Qed.
 
 Goal forall x y z, implb ((x <=? 3) && ((y <=? 7) || (z <=? 9)))
                          ((x + y <=? 10) || (x + z <=? 12)) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
 (* lia2.smt *)
 
 Goal forall x, implb (x - 3 =? 7) (x >=? 10) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
 (* lia3.smt *)
 
 Goal forall x y, implb (x >? y) (y + 1 <=? x) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
 (* lia4.smt *)
 
 Goal forall x y, Bool.eqb (x <? y) (x <=? y - 1) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -387,21 +398,21 @@ Qed.
 
 Goal forall x y, ((x + y <=? - (3)) && (y >=? 0)
                   || (x <=? - (3))) && (x >=? 0) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 (* lia6.smt *)
 
 Goal forall x, implb (andb ((x - 3) <=? 7) (7 <=? (x - 3))) (x >=? 10) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
 (* lia7.smt *)
 
 Goal forall x, implb (x - 3 =? 7) (10 <=? x) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -409,7 +420,7 @@ Qed.
 
 Lemma irrelf_ltb a b c:
   (Z.ltb a b) && (Z.ltb b c) && (Z.ltb c a) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -419,20 +430,20 @@ Lemma comp f g (x1 x2 x3 : Z) :
            (Z.eqb x1 (f (g x3)))
            true)
       true.
-Proof. verit. Qed.
+Proof using. verit. Qed.
 
 
 (* More general examples *)
 
 Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 
 Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
     (negb (f a =? b)) || (negb (P (f a))) || (P b).
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -443,7 +454,7 @@ Goal forall b1 b2 x1 x2,
            (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2))
            (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2)))
       ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)).
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -453,21 +464,21 @@ Qed.
 Goal forall b,
     let a := b in
     a && (negb a) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 Goal forall b,
     let a := b in
     a || (negb a) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 (* Does not work since the [is_true] coercion includes [let in]
 Goal forall b,
   let a := b in
   a || (negb a).
-Proof.
+Proof using.
   verit.
 Qed.
 *)
@@ -477,27 +488,27 @@ Qed.
 Goal forall i j,
     let a := i == j in
     a && (negb a) = false.
-Proof.
+Proof using.
   verit.
 Qed.
 
 Goal forall i j,
     let a := i == j in
     a || (negb a) = true.
-Proof.
+Proof using.
   verit.
 Qed.
 
 (* TODO: fails with native-coq: "compilation error"
 Goal forall (i j:int),
     (i == j) && (negb (i == j)) = false.
-Proof.
+Proof using.
   verit.
   exact int63_compdec.
 Qed.
 
 Goal forall i j, (i == j) || (negb (i == j)).
-Proof.
+Proof using.
   verit.
   exact int63_compdec.
 Qed.
@@ -508,13 +519,13 @@ Qed.
 
 Goal forall (f:Z -> Z -> Z) x y z,
     implb (x =? y) (f z x =? f z y).
-Proof.
+Proof using.
   verit.
 Qed.
 
 Goal forall (P:Z -> Z -> bool) x y z,
     implb (x =? y) (implb (P z x) (P z y)).
-Proof.
+Proof using.
   verit.
 Qed.
 
@@ -524,80 +535,80 @@ Qed.
 
 Lemma taut1 :
   forall f, f 2 =? 0 -> f 2 =? 0.
-Proof. intros f p. verit p. Qed.
+Proof using. intros f p. verit p. Qed.
 
 Lemma taut2 :
   forall f, 0 =? f 2 -> 0 =?f 2.
-Proof. intros f p. verit p. Qed.
+Proof using. intros f p. verit p. Qed.
 
 Lemma taut3 :
   forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0.
-Proof. intros f p1 p2. verit p1 p2. Qed.
+Proof using. intros f p1 p2. verit p1 p2. Qed.
 
 Lemma taut4 :
   forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0.
-Proof. intros f p1 p2. verit p1 p2. Qed.
+Proof using. intros f p1 p2. verit p1 p2. Qed.
 
 Lemma test_eq_sym a b : implb (a =? b) (b =? a).
-Proof. verit. Qed.
+Proof using. verit. Qed.
 
 Lemma taut5 :
   forall f, 0 =? f 2 -> f 2 =? 0.
-Proof. intros f p. verit p. Qed.
+Proof using. intros f p. verit p. Qed.
 
 Lemma fun_const_Z :
   forall f , (forall x, f x =? 2) ->
              f 3 =? 2.
-Proof. intros f Hf. verit Hf. Qed.
+Proof using. intros f Hf. verit Hf. Qed.
 
 Lemma lid (A : bool) :  A -> A.
-Proof. intro a. verit a. Qed.
+Proof using. intro a. verit a. Qed.
 
 Lemma lpartial_id A :
   (xorb A A) -> (xorb A A).
-Proof. intro xa. verit xa. Qed.
+Proof using. intro xa. verit xa. Qed.
 
 Lemma llia1 X Y Z:
   (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) ->
   (X + Y <=? 10) || (X + Z <=? 12).
-Proof. intro p. verit p. Qed.
+Proof using. intro p. verit p. Qed.
 
 Lemma llia2 X:
   X - 3 =? 7 -> X >=? 10.
-Proof. intro p. verit p. Qed.
+Proof using. intro p. verit p. Qed.
 
 Lemma llia3 X Y:
   X >? Y -> Y + 1 <=? X.
-Proof. intro p. verit p. Qed.
+Proof using. intro p. verit p. Qed.
 
 Lemma llia6 X:
   andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10.
-Proof. intro p. verit p. Qed.
+Proof using. intro p. verit p. Qed.
 
 Lemma even_odd b1 b2 x1 x2:
   (ifb b1
        (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2))
        (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) ->
   ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)).
-Proof. intro p. verit p. Qed.
+Proof using. intro p. verit p. Qed.
 
 Lemma lcongr1 (a b : Z) (P : Z -> bool) f:
   (f a =? b) -> (P (f a)) -> P b.
-Proof. intros eqfab pfa. verit eqfab pfa. Qed.
+Proof using. intros eqfab pfa. verit eqfab pfa. Qed.
 
 Lemma lcongr2 (f:Z -> Z -> Z) x y z:
   x =? y -> f z x =? f z y.
-Proof. intro p. verit p. Qed.
+Proof using. intro p. verit p. Qed.
 
 Lemma lcongr3 (P:Z -> Z -> bool) x y z:
   x =? y -> P z x -> P z y.
-Proof. intros eqxy pzx. verit eqxy pzx. Qed.
+Proof using. intros eqxy pzx. verit eqxy pzx. Qed.
 
 Lemma test20 :  forall x, (forall a, a <? x) -> 0 <=? x = false.
-Proof. intros x H. verit H. Qed.
+Proof using. intros x H. verit H. Qed.
 
 Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x).
-Proof. intros x H. verit H. Qed.
+Proof using. intros x H. verit H. Qed.
 
 Lemma un_menteur (a b c d : Z) dit:
   dit a =? c ->
@@ -606,13 +617,13 @@ Lemma un_menteur (a b c d : Z) dit:
   (a =? c) || (a =? d) ->
   (b =? c) || (b =? d) ->
   a =? d.
-Proof. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed.
+Proof using. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed.
 
 Lemma const_fun_is_eq_val_0 :
   forall f : Z -> Z,
     (forall a b, f a =? f b) ->
     forall x, f x =? f 0.
-Proof. intros f Hf. verit Hf. Qed.
+Proof using. intros f Hf. verit Hf. Qed.
 
 (* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to
    the environment. If you did so in a section then, at the end of the section,
@@ -624,7 +635,7 @@ Section S.
   Hypothesis th : forall x, Z.eqb (f x) 3.
   Add_lemmas th.
   Goal forall x, Z.eqb ((f x) + 1) 4.
-  Proof. verit. Qed.
+  Proof using th. verit. Qed.
   Clear_lemmas.
 End S.
 
@@ -635,7 +646,7 @@ Section fins_sat6.
   Add_lemmas andab orcd.
 
   Lemma sat6 :  orb c (andb a (andb b d)).
-  Proof. verit. Qed.
+  Proof using andab orcd. verit. Qed.
   Clear_lemmas.
 End fins_sat6.
 
@@ -649,7 +660,7 @@ Section fins_lemma_multiple.
   Add_lemmas g_k_linear f'_equal_k.
 
   Lemma apply_lemma_multiple : forall x y, g (x + 1) =? g x + f' y.
-  Proof. verit. Qed.
+  Proof using g_k_linear f'_equal_k. verit. Qed.
 
   Clear_lemmas.
 End fins_lemma_multiple.
@@ -661,11 +672,11 @@ Section fins_find_apply_lemma.
   Add_lemmas u_is_constant.
 
   Lemma apply_lemma : forall x, u x =? u 2.
-  Proof. verit. Qed.
+  Proof using u_is_constant. verit. Qed.
 
   Lemma find_inst :
     implb (u 2 =? 5) (u 3 =? 5).
-  Proof. verit. Qed.
+  Proof using u_is_constant. verit. Qed.
 
   Clear_lemmas.
 End fins_find_apply_lemma.
@@ -678,7 +689,7 @@ Section mult3.
   Add_lemmas mult3_0 mult3_Sn.
 
   Lemma mult3_4_12 : mult3 4 =? 12.
-  Proof. verit. Qed. (* slow to verify with standard coq *)
+  Proof using mult3_0 mult3_Sn. verit. Qed. (* slow to verify with standard coq *)
 
   Clear_lemmas.
 End mult3.
@@ -691,7 +702,7 @@ End mult3.
 (*   Hypothesis mult_Sx : forall x y, mult (x+1) y =? mult x y + y. *)
 
 (*   Lemma mult_1_x : forall x, mult 1 x =? x. *)
-(*   Proof. verit mult_0 mult_Sx. *)
+(*   Proof using. verit mult_0 mult_Sx. *)
 (*   Qed. *)
 (* End mult. *)
 
@@ -704,7 +715,7 @@ Section implicit_transform.
 
   Lemma implicit_transform :
     f a2.
-  Proof. verit. Qed.
+  Proof using f_const f_a1. verit. Qed.
 
   Clear_lemmas.
 End implicit_transform.
@@ -724,23 +735,23 @@ Section list.
 
   Lemma in_cons1 :
     inlist 1 (1::2::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons. verit. Qed.
 
   Lemma in_cons2 :
     inlist 12 (2::4::12::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons. verit. Qed.
 
   Lemma in_cons3 :
     inlist 1 (5::1::(0-1)::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons. verit. Qed.
 
   Lemma in_cons4 :
     inlist 22 ((- (1))::22::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons. verit. Qed.
 
   Lemma in_cons5 :
     inlist 1 ((- 1)::1::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons. verit. Qed.
 
   (* Lemma in_cons_false1 : *)
   (*   inlist 1 (2::3::nil). *)
@@ -764,15 +775,15 @@ Section list.
 
   Lemma in_app1 :
     inlist 1 (1::2::nil ++ nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed.
 
   Lemma in_app2 :
     inlist 1 (nil ++ 2::1::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed.
 
   Lemma in_app3 :
     inlist 1 (1::3::nil ++ 2::1::nil).
-  Proof. verit. Qed.
+  Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed.
 
   (* Lemma in_app_false1 : *)
   (*   inlist 1 (nil ++ 2::3::nil). *)
@@ -802,7 +813,7 @@ Section list.
   Lemma coqhammer_example l1 l2 x y1 y2 y3:
     implb (orb (inlist x l1) (orb (inlist x l2) (orb (x =? y1) (inlist x (y2 ::y3::nil)))))
           (inlist x (y1::(l1 ++ (y2 :: (l2 ++ (y3 :: nil)))))).
-  Proof. verit_no_check. Qed.
+  Proof using dec_Zlist in_eq in_cons in_or_app in_nil in_inv inlist_app_comm_cons. verit_no_check. Qed.
 
   Clear_lemmas.
 End list.
@@ -823,59 +834,59 @@ Section group.
 
   Lemma unique_identity e':
     (forall z, op e' z =? z) -> e' =? e.
-  Proof. intros pe'. verit pe'. Qed.
+  Proof using associative identity inverse. intros pe'. verit pe'. Qed.
 
   Lemma simplification_right x1 x2 y:
       op x1 y =? op x2 y -> x1 =? x2.
-  Proof. intro H. verit H. Qed.
+  Proof using associative identity inverse. intro H. verit H. Qed.
 
   Lemma simplification_left x1 x2 y:
       op y x1 =? op y x2 -> x1 =? x2.
-  Proof. intro H. verit H. Qed.
+  Proof using associative identity inverse. intro H. verit H. Qed.
 
   Clear_lemmas.
 End group.
 
 Section Linear1.
-  Parameter f : Z -> Z.
-  Axiom f_spec : forall x,  (f (x+1) =? f x + 1)  && (f 0 =? 0).
+  Variable f : Z -> Z.
+  Hypothesis f_spec : forall x,  (f (x+1) =? f x + 1)  && (f 0 =? 0).
 
   (* Cuts are not automatically proved when one equality is switched *)
   Lemma f_1 : f 1 =? 1.
-  Proof.
+  Proof using f_spec.
     verit_bool f_spec; replace (0 =? f 0) with (f 0 =? 0) by apply Z.eqb_sym; auto.
   Qed.
 End Linear1.
 
 Section Linear2.
-  Parameter g : Z -> Z.
+  Variable g : Z -> Z.
 
-  Axiom g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2).
+  Hypothesis g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2).
 
 (* The call to veriT does not terminate *)
 (* Lemma apply_lemma_infinite : *)
 (*   forall x y, Z.eqb (g (x + y)) ((g x) + y * 2). *)
-(* Proof. verit g_2_linear. *)
+(* Proof using. verit g_2_linear. *)
 End Linear2.
 
 Section Input_switched1.
-  Parameter m : Z -> Z.
+  Variable m : Z -> Z.
 
-  Axiom m_0 : m 0 =? 5.
+  Hypothesis m_0 : m 0 =? 5.
 
   (* veriT switches the input lemma in this case *)
   Lemma cinq_m_0 : m 0 =? 5.
-  Proof. verit m_0. Qed.
+  Proof using m_0. verit m_0. Qed.
 End Input_switched1.
 
 Section Input_switched2.
-  Parameter h : Z -> Z -> Z.
+  Variable h : Z -> Z -> Z.
 
-  Axiom h_Sm_n : forall x y, h (x+1) y =? h x y.
+  Hypothesis h_Sm_n : forall x y, h (x+1) y =? h x y.
 
   (* veriT switches the input lemma in this case *)
   Lemma h_1_0 : h 1 0 =? h 0 0.
-  Proof. verit h_Sm_n. Qed.
+  Proof using h_Sm_n. verit h_Sm_n. Qed.
 End Input_switched2.
 
 
@@ -887,7 +898,7 @@ Goal forall (f : positive -> positive) (x y : positive),
   implb ((x + 3) =? y)
         ((f (x + 3)) <=? (f y))
   = true.
-Proof.
+Proof using.
 pos_convert.
 verit.
 Qed.
@@ -896,7 +907,7 @@ Goal forall (f : positive -> positive) (x y : positive),
   implb ((x + 3) =? y)
         ((3 <? y) && ((f (x + 3)) <=? (f y)))
   = true.
-Proof.
+Proof using.
 pos_convert.
 verit.
 Qed.
@@ -909,7 +920,7 @@ Goal forall (f : N -> N) (x y : N),
   implb ((x + 3) =? y)
         ((f (x + 3)) <=? (f y))
   = true.
-Proof.
+Proof using.
 N_convert.
 verit.
 Qed.
@@ -918,7 +929,7 @@ Goal forall (f : N -> N) (x y : N),
   implb ((x + 3) =? y)
         ((2 <? y) && ((f (x + 3)) <=? (f y)))
   = true.
-Proof.
+Proof using.
 N_convert.
 verit.
 Qed.
@@ -932,7 +943,7 @@ Goal forall (f : nat -> nat) (x y : nat),
   implb (Nat.eqb (x + 3) y)
         ((f (x + 3)) <=? (f y))
   = true.
-Proof.
+Proof using.
 nat_convert.
 verit.
 Qed.
@@ -941,7 +952,7 @@ Goal forall (f : nat -> nat) (x y : nat),
   implb (Nat.eqb (x + 3) y)
         ((2 <? y) && ((f (x + 3)) <=? (f y)))
   = true.
-Proof.
+Proof using.
 nat_convert.
 verit.
 Qed.
@@ -954,6 +965,7 @@ Goal forall f : positive -> nat -> N, forall (x : positive) (y : nat),
     (implb (Nat.eqb y 7)
       (implb (f 3%positive 7%nat =? 12)%N
         (f x y =? 12)%N)) = true.
+Proof using.
 pos_convert.
 nat_convert.
 N_convert.
diff --git a/unit-tests/Tests_zchaff_tactics.v b/unit-tests/Tests_zchaff_tactics.v
index c6ed4e3..cf86bc1 100644
--- a/unit-tests/Tests_zchaff_tactics.v
+++ b/unit-tests/Tests_zchaff_tactics.v
@@ -23,7 +23,7 @@ Local Open Scope int63_scope.
 
 Lemma check_univ (x1: bool):
   (x1 && (negb x1)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -31,55 +31,67 @@ Qed.
 (* zChaff tactic *)
 
 Goal forall a, a || negb a.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, negb (a || negb a) = false.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, negb (negb (a || negb a)).
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, (a && negb a) = false.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, negb (a && negb a).
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, implb a a.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, negb (implb a a) = false.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a , (xorb a a) || negb (xorb a a).
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, (a||negb a) || negb (a||negb a).
+Proof using.
   zchaff.
 Qed.
 
 Goal true.
+Proof using.
   zchaff.
 Qed.
 
 Goal negb false.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall a, Bool.eqb a a.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 Goal forall (a:bool), a = a.
+Proof using.
   zchaff.
 Qed.
 
@@ -88,7 +100,7 @@ Qed.
 (* ((a ∧ b) ∨ (b ∧ c)) ∧ ¬b = ⊥ *)
 
 Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -97,7 +109,7 @@ Qed.
 (* (a ∨ a) ∧ ¬a = ⊥ *)
 
 Goal forall a, ((a || a) && (negb a)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -106,7 +118,7 @@ Qed.
 (* ¬(a ∨ ¬a) = ⊥ *)
 
 Goal forall a, (negb (a || (negb a))) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -116,7 +128,7 @@ Qed.
 
 Goal forall a b c,
   (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -125,7 +137,7 @@ Qed.
 
 Goal forall i j k,
   ((i == j) || (j == k) || (k == i)) && ((negb (i == j)) || (negb (j == k)) || (negb (k == i))) && ((negb (i == j)) || (j == k)) && ((negb (j == k)) || (k == i)) && ((negb (k == i)) || (i == j)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -134,7 +146,7 @@ Goal forall i j k,
   let b := j == k in
   let c := k == i in
   (a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -143,7 +155,7 @@ Qed.
 (* (a ∧ b) ∧ (c ∨ d) ∧ ¬(c ∨ (a ∧ b ∧ d)) = ⊥ *)
 
 Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -152,7 +164,7 @@ Qed.
 (* a ∧ b ∧ c ∧ (¬a ∨ ¬b ∨ d) ∧ (¬d ∨ ¬c) = ⊥ *)
 
 Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -160,37 +172,37 @@ Qed.
 (* Other connectives *)
 
 Goal (false || true) && false = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 
 Goal negb true = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 
 Goal false = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 
 Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)).
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 
 Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)).
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 
 Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)).
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -198,7 +210,7 @@ Qed.
 (* Multiple negations *)
 
 Goal forall a, orb a (negb (negb (negb a))) = true.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -206,13 +218,13 @@ Qed.
 (* Polarities *)
 
 Goal forall a b, andb (orb a b) (negb (orb a b)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
 
 Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -307,7 +319,7 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42
   (orb (orb (orb x13 x23) x33) x43) &&
   (orb (orb (orb x14 x24) x34) x44) &&
   (orb (orb (orb x15 x25) x35) x45)) = false.
-Proof.
+Proof using.
   zchaff.
 Qed.
 
@@ -316,12 +328,12 @@ Qed.
 
 (*
 Goal forall x, x && (negb x).
-Proof.
+Proof using.
   zchaff.
 Abort.
 
 Goal forall x y, (implb (implb x y) (implb y x)).
-Proof.
+Proof using.
   zchaff.
 Abort.
 
@@ -391,7 +403,7 @@ Goal forall x11 x12 x13 x14 x21 x22 x23 x24 x31 x32 x33 x34 x41 x42 x43 x44, (
   (orb (orb (orb x12 x22) x32) x42) &&
   (orb (orb (orb x13 x23) x33) x43) &&
   (orb (orb (orb x14 x24) x34) x44)) = false.
-Proof.
+Proof using.
   zchaff.
 Abort.
 *)