Convert hypotheses from Prop to bool (#89)

* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed.

* Some current limitations are detailed in src/PropToBool.v.

* Partially enhances #30 .

12 files changed, 304 insertions, 113 deletions

diff --git a/src/BoolToProp.v b/src/BoolToProp.v
deleted file mode 100644
index 8a3b134..0000000
--- a/src/BoolToProp.v
+++ /dev/null
@@ -1,74 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2019                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-Require Import
-        Bool ZArith BVList Logic BVList FArray
-        SMT_classes SMT_classes_instances ReflectFacts.
-Import BVList.BITVECTOR_LIST. 
-
-Local Coercion is_true : bool >-> Sortclass.
-
-Infix "--->" := implb (at level 60, right associativity) : bool_scope.
-Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
-
-Ltac bool2prop :=
-  repeat
-    match goal with
-    | [ |- forall _ : bitvector _, _] => intro
-    | [ |- forall _ : farray _ _, _] => intro
-    | [ |- forall _ : _ -> _, _] => intro
-    | [ |- forall _ : Z, _] => intro
-    | [ |- forall _ : bool, _] => intro
-    | [ |- forall _ : Type, _] => intro
-    | [ p: Type |-  context[ forall _ : ?t, _ ] ] => intro
-
-    | [ |- forall t : Type, CompDec t -> _  ] => intro
-    | [ |- CompDec _ -> _  ] => intro
-
-    | [ |- context[ bv_ult _ _ ] ] => unfold is_true; rewrite bv_ult_B2P
-    | [ |- context[ bv_slt _ _ ] ] => unfold is_true; rewrite bv_slt_B2P
-    | [ |- context[ bv_eq _ _ ] ]  => unfold is_true; rewrite bv_eq_reflect
-    | [ |- context[ equal _ _ ] ]  => unfold is_true; rewrite equal_iff_eq
-    | [ |- context[ Z.ltb _ _ ] ]  => unfold is_true; rewrite Z.ltb_lt
-    | [ |- context[ Z.gtb _ _ ] ]  => unfold is_true; rewrite Z.gtb_lt
-    | [ |- context[ Z.leb _ _ ] ]  => unfold is_true; rewrite Z.leb_le
-    | [ |- context[ Z.geb _ _ ] ]  => unfold is_true; rewrite Z.geb_le
-    | [ |- context[ Z.eqb _ _ ] ]  => unfold is_true; rewrite Z.eqb_eq
-
-    | [ |- context[?G0 ---> ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true -> G1 = true)  (G0 ---> G1)); 
-      [ | apply implyP]
-
-    | [ |- context[?G0 || ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1)); 
-      [ | apply orP]
-
-    | [ |- context[?G0 && ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (G0 && G1)); 
-      [ | apply andP]
-
-    | [ |- context[?G0 <---> ?G1 ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (G0 <---> G1)); 
-      [ | apply iffP]
-
-    | [ |- context[ negb ?G ] ] =>
-      unfold is_true; rewrite <- (@reflect_iff (G <> true) (negb G)); 
-      [ | apply negP]
-
-    | [R : CompDec ?t |- context[ CompDec ?t  ] ] => exact R
-
-    | [R : EqbType ?t |- context[ EqbType ?t  ] ] => exact R
-
-    | [ |- context[ false = true ] ] => rewrite FalseB
-                                              
-    | [ |- context[ true = true ] ] => rewrite TrueB
-
-    end.
diff --git a/src/PropToBool.v b/src/PropToBool.v
index a9cbded..25662ad 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -13,7 +13,13 @@
 Require Import
         Bool ZArith BVList Logic BVList FArray
         SMT_classes SMT_classes_instances ReflectFacts.
-Import BVList.BITVECTOR_LIST. 
+Import BVList.BITVECTOR_LIST.
+
+
+Lemma geb_ge (n m : Z) : (n >=? m)%Z = true <-> (n >= m)%Z.
+Proof.
+  now rewrite Z.geb_le, Z.ge_le_iff.
+Qed.
 
 Ltac prop2bool :=
   repeat
@@ -27,9 +33,9 @@ Ltac prop2bool :=
     | [ |- context[ bv_ultP _ _ ] ] => rewrite <- bv_ult_B2P
     | [ |- context[ bv_sltP _ _ ] ] => rewrite <- bv_slt_B2P
     | [ |- context[ Z.lt _ _ ] ] => rewrite <- Z.ltb_lt
-    | [ |- context[ Z.gt _ _ ] ] => rewrite Z.gt_lt_iff; rewrite <- Z.ltb_lt
+    | [ |- context[ Z.gt _ _ ] ] => rewrite Zgt_is_gt_bool
     | [ |- context[ Z.le _ _ ] ] => rewrite <- Z.leb_le
-    | [ |- context[ Z.ge _ _ ] ] => rewrite Z.ge_le_iff; rewrite <- Z.leb_le
+    | [ |- context[ Z.ge _ _ ] ] => rewrite <- geb_ge
     | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq
 
     | [ |- context[ @Logic.eq ?t _ _ ] ] =>
@@ -77,7 +83,243 @@ Ltac prop2bool :=
     | [ |- context[ True ] ] => rewrite <- TrueB
 
     | [ |- context[ False ] ] => rewrite <- FalseB
+    end.
 
-    (* | [ |- _ : (CompDec _ )] => try easy *)
+
+Ltac bool2prop_true :=
+  repeat
+    match goal with
+    | [ |- forall _ : ?t, _ ] =>
+      lazymatch type of t with
+      | Prop => fail
+      | _ => intro
+      end
+
+    | [ |- context[ bv_ult _ _ = true ] ] => rewrite bv_ult_B2P
+    | [ |- context[ bv_slt _ _ = true ] ] => rewrite bv_slt_B2P
+    | [ |- context[ Z.ltb _ _ = true ] ] => rewrite Z.ltb_lt
+    | [ |- context[ Z.gtb _ _ ] ] => rewrite <- Zgt_is_gt_bool
+    | [ |- context[ Z.leb _ _ = true ] ] => rewrite Z.leb_le
+    | [ |- context[ Z.geb _ _ ] ] => rewrite geb_ge
+    | [ |- context[ Z.eqb _ _ = true ] ] => rewrite Z.eqb_eq
+
+    | [ |- context[ eqb_of_compdec ?p _ _ = true ] ] => rewrite <- (@compdec_eq_eqb _ p)
+
+    | [ |- context[ ?G0 || ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1));
+      [ | apply orP]
+
+    | [ |- context[ implb ?G0 ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1));
+      [ | apply implyP]
+
+    | [ |- context[?G0 && ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1));
+      [ | apply andP]
+
+    | [ |- context[Bool.eqb ?G0 ?G1 = true ] ] =>
+      rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1));
+      [ | apply iffP]
+
+    | [ |- context[ negb ?G = true ] ] =>
+      rewrite <- (@reflect_iff (~ G = true) (negb G));
+      [ | apply negP]
+
+    | [ |- context[ true = true ] ] => rewrite TrueB
+
+    | [ |- context[ false = true ] ] => rewrite FalseB
     end.
 
+Ltac bool2prop := unfold is_true; bool2prop_true.
+
+
+Ltac prop2bool_hyp H :=
+  let TH := type of H in
+
+  (* Add a CompDec hypothesis if needed *)
+  let prop2bool_t := fresh "prop2bool_t" in epose (prop2bool_t := ?[prop2bool_t_evar] : Type);
+  let prop2bool_comp := fresh "prop2bool_comp" in epose (prop2bool_comp := ?[prop2bool_comp_evar] : bool);
+  let H' := fresh in
+  assert (H':False -> TH);
+  [ let HFalse := fresh "HFalse" in intro HFalse;
+    repeat match goal with
+           | [ |- forall _ : ?t, _ ] =>
+             lazymatch type of t with
+             | Prop => fail
+             | _ => intro
+             end
+           | [ |- context[@eq ?A _ _] ] => instantiate (prop2bool_t_evar := A); instantiate (prop2bool_comp_evar := true)
+           | _ => instantiate (prop2bool_t_evar := nat); instantiate (prop2bool_comp_evar := false)
+           end;
+    destruct HFalse
+  | ];
+  clear H';
+  match (eval compute in prop2bool_comp) with
+  | true =>
+    let A := eval cbv in prop2bool_t in
+    match goal with
+    | [ _ : CompDec A |- _ ] => idtac
+    | _ =>
+      let Hcompdec := fresh "Hcompdec" in
+      assert (Hcompdec: CompDec A);
+      [ auto with typeclass_instances | ]
+    end
+  | false => idtac
+  end;
+  clear prop2bool_t; clear prop2bool_comp;
+
+  (* Compute the bool version of the lemma *)
+  [ .. |
+    let prop2bool_Hbool := fresh "prop2bool_Hbool" in epose (prop2bool_Hbool := ?[prop2bool_Hbool_evar] : Prop);
+    assert (H':False -> TH);
+    [ let HFalse := fresh "HFalse" in intro HFalse;
+      let rec tac_rec :=
+          match goal with
+          | [ |- forall _ : ?t, _ ] =>
+            lazymatch type of t with
+            | Prop => fail
+            | _ =>
+              let H := fresh in
+              intro H; tac_rec; revert H
+            end
+          | _ => prop2bool
+          end in
+      tac_rec;
+      match goal with
+      | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g
+      end;
+      destruct HFalse
+    | ];
+    clear H';
+
+    (* Assert and prove the bool version of the lemma *)
+    assert (H':prop2bool_Hbool); subst prop2bool_Hbool;
+    [ bool2prop; apply H | ];
+
+    (* Replace the Prop version with the bool version *)
+    clear H; assert (H:=H'); clear H'
+  ].
+
+Ltac prop2bool_hyps Hs :=
+  match Hs with
+  | (?Hs, ?H) => try prop2bool_hyp H; [ .. | prop2bool_hyps Hs]
+  | ?H => try prop2bool_hyp H
+  end.
+
+
+
+Section Test.
+  Variable A : Type.
+
+  Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
+  Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
+  Hypothesis uninterpreted_type : forall (a:A), a = a.
+
+  Goal True.
+  Proof.
+    prop2bool_hyp basic.
+    prop2bool_hyp no_eq.
+    prop2bool_hyp uninterpreted_type.
+  Abort.
+
+  Goal True.
+  Proof.
+    prop2bool_hyps (basic, no_eq, uninterpreted_type).
+  Abort.
+End Test.
+
+Section Group.
+
+  Variable G : Type.
+  Variable HG : CompDec G.
+  Variable op : G -> G -> G.
+  Variable inv : G -> G.
+  Variable e : G.
+
+  Hypothesis associative :
+    forall a b c : G, op a (op b c) = op (op a b) c.
+  Hypothesis identity :
+    forall a : G, (op e a = a) /\ (op a e = a).
+  Hypothesis inverse :
+    forall a : G, (op a (inv a) = e) /\ (op (inv a) a = e).
+
+  Variable e' : G.
+  Hypothesis other_id : forall e' z, op e' z = z.
+
+  Goal True.
+  Proof.
+    prop2bool_hyp associative.
+    prop2bool_hyp identity.
+    prop2bool_hyp inverse.
+    prop2bool_hyp other_id.
+    exact I.
+  Qed.
+
+  Goal True.
+  Proof.
+    prop2bool_hyps (associative, identity, inverse, other_id).
+    exact I.
+  Qed.
+
+End Group.
+
+
+Section MultipleCompDec.
+
+  Variables A B : Type.
+  Hypothesis multiple : forall (a1 a2:A) (b1 b2:B), a1 = a2 -> b1 = b2.
+
+  Goal True.
+  Proof.
+    Fail prop2bool_hyp multiple.
+  Abort.
+
+End MultipleCompDec.
+
+
+(* We can assume that we deal only with monomorphic hypotheses, since
+   polymorphism will be removed before *)
+Section Poly.
+  Hypothesis basic : forall (A:Type) (l1 l2:list A),
+    length (l1++l2) = length l1 + length l2.
+  Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
+
+  Goal True.
+  Proof.
+    prop2bool_hyp basic.
+    Fail prop2bool_hyp uninterpreted_type.
+  Abort.
+
+End Poly.
+
+
+
+
+
+Infix "--->" := implb (at level 60, right associativity) : bool_scope.
+Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope.
+
+
+
+(* Does not fail since 8.10 *)
+
+Goal True.
+  evar (t:Type).
+  assert (H:True).
+  - instantiate (t:=nat). exact I.
+  - exact I.
+Qed.
+
+Goal True.
+  evar (t:option Set).
+  assert (H:True).
+  - instantiate (t:=Some nat). exact I.
+  - exact I.
+Qed.
+
+Goal True.
+  evar (t:option Type).
+  assert (H:True).
+  - Fail instantiate (t:=Some nat). exact I.
+  - exact I.
+Abort.
diff --git a/src/SMTCoq.v b/src/SMTCoq.v
index 6b69058..398d066 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Export PropToBool BoolToProp.  (* Before SMTCoq.State *)
+Require Export PropToBool.
 Require Export Int63 List PArray.
 Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances.
 Require Export Tactics.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 89d6c62..50c02b7 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -764,6 +764,7 @@ End list.
 Hint Resolve unit_ord unit_eqbtype unit_comp unit_inh unit_compdec : typeclass_instances.
 Hint Resolve bool_ord bool_eqbtype bool_dec bool_comp bool_inh bool_compdec : typeclass_instances.
 Hint Resolve Z_ord Z_eqbtype Z_dec Z_comp Z_inh Z_compdec : typeclass_instances.
+Hint Resolve Nat_ord Nat_eqbtype Nat_dec Nat_comp Nat_inh Nat_compdec : typeclass_instances.
 Hint Resolve Positive_ord Positive_eqbtype Positive_dec Positive_comp Positive_inh Positive_compdec : typeclass_instances.
 Hint Resolve BV_ord BV_eqbtype BV_dec BV_comp BV_inh BV_compdec : typeclass_instances.
 Hint Resolve FArray_ord FArray_eqbtype FArray_dec FArray_comp FArray_inh FArray_compdec : typeclass_instances.
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index a6d0023..ca5f3cc 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -355,7 +355,6 @@ let rec mk_bv_list = function
 
 
 (* Reification *)
-
 let mk_bool b =
   let c, args = Structures.decompose_app b in
   if Structures.eq_constr c (Lazy.force ctrue) then true
@@ -435,3 +434,27 @@ let mk_bvsize n =
       else assert false
     | _ -> assert false
   else mk_N n
+
+(** Switches between constr and OCaml *)
+(* Transform a option constr into a constr option *)
+let option_of_constr_option co =
+  let c, args = Structures.decompose_app co in
+  if c = Lazy.force cSome then
+    match args with
+      | [_;c] -> Some c
+      | _ -> assert false
+  else
+    None
+
+(* Transform a tuple of constr into a (reversed) list of constr *)
+let list_of_constr_tuple =
+  let rec list_of_constr_tuple acc t =
+    let c, args = Structures.decompose_app t in
+    if c = Lazy.force cpair then
+      match args with
+        | [_;_;t;l] -> list_of_constr_tuple (l::acc) t
+        | _ -> assert false
+    else
+      t::acc
+  in
+  list_of_constr_tuple []
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index bf626b3..b5ca6b7 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -261,3 +261,7 @@ val mk_nat : Structures.constr -> int
 val mk_N : Structures.constr -> int
 val mk_Z : Structures.constr -> int
 val mk_bvsize : Structures.constr -> int
+
+(* Switches between constr and OCaml *)
+val option_of_constr_option : Structures.constr -> Structures.constr option
+val list_of_constr_tuple : Structures.constr -> Structures.constr list
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 92f0f09..aad8b07 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -23,8 +23,8 @@ let mkInt i =
 (** Generic representation of shared object *)
 type 'a gen_hashed = { index : int; hval : 'a }
 
-(** Functions over constr *)
 
+(** Functions over constr *)
 let mklApp f args = Structures.mkApp (Lazy.force f, args)
 
 let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index fbc04e3..3080372 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -218,6 +218,16 @@ let verit_logic =
   SL.of_list [LUF; LLia]
 
 let tactic_gen vm_cast lcpl lcepl =
+  (* Transform the tuple of lemmas given by the user into a list *)
+  let lcpl =
+    let lcpl = EConstr.Unsafe.to_constr lcpl in
+    let lcpl = CoqTerms.option_of_constr_option lcpl in
+    match lcpl with
+      | Some lcpl -> CoqTerms.list_of_constr_tuple lcpl
+      | None -> []
+  in
+
+  (* Core tactic *)
   clear_all ();
   let rt = SmtBtype.create () in
   let ro = Op.create () in
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 6fa62d8..4b84b58 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -19,5 +19,5 @@ val parse_certif :
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
 val theorem : Structures.id -> string -> string -> unit
-val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic
+val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 4162f13..6ddf5a5 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -10,18 +10,18 @@
 (**************************************************************************)
 
 
-Require Import PropToBool BoolToProp.  (* Before SMTCoq.State *)
+Require Import PropToBool.
 Require Import Int63 List PArray Bool ZArith.
 Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst.
 
 Declare ML Module "smtcoq_plugin".
 
 
-Tactic Notation "verit_bool" constr_list(h) :=
-  verit_bool_base h; vauto.
+Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto.
+Tactic Notation "verit_bool"           := verit_bool_base (@None nat); vauto.
 
-Tactic Notation "verit_bool_no_check" constr_list(h) :=
-  verit_bool_no_check_base h; vauto.
+Tactic Notation "verit_bool_no_check" constr(h) := verit_bool_no_check_base (Some h); vauto.
+Tactic Notation "verit_bool_no_check"           := verit_bool_no_check_base (@None nat); vauto.
 
 
 (** Tactics in Prop **)
@@ -29,32 +29,18 @@ Tactic Notation "verit_bool_no_check" constr_list(h) :=
 Ltac zchaff          := prop2bool; zchaff_bool; bool2prop.
 Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
 
-Tactic Notation "verit" constr_list(h) := prop2bool; [ .. | verit_bool h; bool2prop ].
-Tactic Notation "verit_no_check" constr_list(h) := prop2bool; [ .. | verit_bool_no_check h; bool2prop ].
+Tactic Notation "verit" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool h; bool2prop ] ].
+Tactic Notation "verit"           := prop2bool; [ .. | verit_bool  ; bool2prop ].
+Tactic Notation "verit_no_check" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool_no_check h; bool2prop ] ].
+Tactic Notation "verit_no_check"           := prop2bool; [ .. | verit_bool_no_check  ; bool2prop ].
 
 Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
 Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
-
-(* Ltac smt := prop2bool; *)
-(*             repeat *)
-(*               match goal with *)
-(*                 | [ |- context[ CompDec ?t ] ] => try assumption *)
-(*                 | [ |- _ : bool] => verit_bool *)
-(*                 | [ |- _ : bool] => try (cvc4_bool; verit_bool) *)
-(*               end; *)
-(*             bool2prop. *)
-(* Ltac smt_no_check := prop2bool; *)
-(*             repeat *)
-(*               match goal with *)
-(*                 | [ |- context[ CompDec ?t ] ] => try assumption *)
-(*                 | [ |- _ : bool] => verit_bool_no_check *)
-(*                 | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *)
-(*               end; *)
-(*             bool2prop. *)
-
-Tactic Notation "smt" constr_list(h) := (prop2bool; [ .. | try verit_bool h; cvc4_bool; try verit_bool h; bool2prop ]).
-Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; [ .. | try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; bool2prop]).
+Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool h ]); cvc4_bool; try (prop2bool_hyps h; [ .. | verit_bool h ]); bool2prop ]).
+Tactic Notation "smt"           := (prop2bool; [ .. | try verit_bool  ; cvc4_bool; try verit_bool  ; bool2prop ]).
+Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); cvc4_bool_no_check; try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); bool2prop]).
+Tactic Notation "smt_no_check"           := (prop2bool; [ .. | try verit_bool_no_check  ; cvc4_bool_no_check; try verit_bool_no_check  ; bool2prop]).
 
 
 
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
index e067da8..86dd443 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/versions/standard/_CoqProject
@@ -149,7 +149,6 @@ Misc.v
 SMTCoq.v
 ReflectFacts.v
 PropToBool.v
-BoolToProp.v
 QInst.v
 Tactics.v
 SMT_terms.v
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4
index 6c3b8cf..2411316 100644
--- a/src/versions/standard/g_smtcoq_standard.ml4
+++ b/src/versions/standard/g_smtcoq_standard.ml4
@@ -109,8 +109,8 @@ END
 
 
 TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ]
-| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ]
+| [ "verit_bool_base" constr(lpl) ] -> [ Verit.tactic lpl (get_lemmas ()) ]
+| [ "verit_bool_no_check_base" constr(lpl) ] -> [ Verit.tactic_no_check lpl (get_lemmas ()) ]
 END
 
 TACTIC EXTEND Tactic_cvc4