From 39b4d1d31c6446c937164039cac585dbe91b8b29 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 26 Apr 2021 16:54:56 +0200
Subject: CompDec are automatically discharged when generated by the OCaml
 tactic, when possible

---
 src/versions/standard/Tactics_standard.v | 31 +++++++++++++++++--------------
 unit-tests/Tests_verit_tactics.v         | 17 +++++++++++++----
 2 files changed, 30 insertions(+), 18 deletions(-)

diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 468de7a..232ae54 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -66,25 +66,28 @@ End Test.
 
 (** Tactics in bool *)
 
+Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; auto with typeclass_instances.
+Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; auto with typeclass_instances.
+
 Tactic Notation "verit_bool" constr(h) :=
   get_hyps ltac:(fun Hs =>
                    match Hs with
-                   | Some ?Hs => verit_bool_base (Some (h, Hs))
-                   | None => verit_bool_base (Some h)
+                   | Some ?Hs => verit_bool_base_auto (Some (h, Hs))
+                   | None => verit_bool_base_auto (Some h)
                    end;
                    vauto).
 Tactic Notation "verit_bool"           :=
-  get_hyps ltac:(fun Hs => verit_bool_base Hs; vauto).
+  get_hyps ltac:(fun Hs => verit_bool_base_auto Hs; vauto).
 
 Tactic Notation "verit_bool_no_check" constr(h) :=
   get_hyps ltac:(fun Hs =>
                    match Hs with
-                   | Some ?Hs => verit_bool_no_check_base (Some (h, Hs))
-                   | None => verit_bool_no_check_base (Some h)
+                   | Some ?Hs => verit_bool_no_check_base_auto (Some (h, Hs))
+                   | None => verit_bool_no_check_base_auto (Some h)
                    end;
                    vauto).
 Tactic Notation "verit_bool_no_check"           :=
-  get_hyps ltac:(fun Hs => verit_bool_no_check_base Hs; vauto).
+  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto Hs; vauto).
 
 
 (** Tactics in Prop **)
@@ -99,8 +102,8 @@ Tactic Notation "verit" constr(h) :=
                                  match Hs with
                                    | Some ?Hs =>
                                      prop2bool_hyps Hs;
-                                     [ .. | verit_bool_base (Some (h, Hs)) ]
-                                   | None => verit_bool_base (Some h)
+                                     [ .. | verit_bool_base_auto (Some (h, Hs)) ]
+                                   | None => verit_bool_base_auto (Some h)
                                  end; vauto)
          ]
   ].
@@ -110,8 +113,8 @@ Tactic Notation "verit"           :=
                           match Hs with
                           | Some ?Hs =>
                             prop2bool_hyps Hs;
-                            [ .. | verit_bool_base (Some Hs) ]
-                          | None => verit_bool_base (@None nat)
+                            [ .. | verit_bool_base_auto (Some Hs) ]
+                          | None => verit_bool_base_auto (@None nat)
                           end; vauto)
   ].
 Tactic Notation "verit_no_check" constr(h) :=
@@ -121,8 +124,8 @@ Tactic Notation "verit_no_check" constr(h) :=
                                  match Hs with
                                    | Some ?Hs =>
                                      prop2bool_hyps Hs;
-                                     [ .. | verit_bool_no_check_base (Some (h, Hs)) ]
-                                   | None => verit_bool_no_check_base (Some h)
+                                     [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ]
+                                   | None => verit_bool_no_check_base_auto (Some h)
                                  end; vauto)
          ]
   ].
@@ -132,8 +135,8 @@ Tactic Notation "verit_no_check"           :=
                           match Hs with
                           | Some ?Hs =>
                             prop2bool_hyps Hs;
-                            [ .. | verit_bool_no_check_base (Some Hs) ]
-                          | None => verit_bool_no_check_base (@None nat)
+                            [ .. | verit_bool_no_check_base_auto (Some Hs) ]
+                          | None => verit_bool_no_check_base_auto (@None nat)
                           end; vauto)
   ].
 
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index a270fdd..73b59f4 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -500,12 +500,21 @@ Qed.
 Goal forall (i j:int),
     (i == j) && (negb (i == j)) = false.
 Proof using.
-  verit. auto with typeclass_instances.
+  verit.
 Qed.
 
+Goal forall (i j:int),
+    ~ ((i = j) /\ (~ (i = j))).
+Proof using. verit. Qed.
+
 Goal forall i j, (i == j) || (negb (i == j)).
 Proof using.
-  verit. auto with typeclass_instances.
+  verit.
+Qed.
+
+Goal forall (i j:int), (i = j) \/ (~ (i = j)).
+Proof using.
+  verit.
 Qed.
 
 
@@ -1153,10 +1162,10 @@ Qed.
 Section AppliedPolymorphicTypes1.
   Goal forall (f : option Z -> Z) (a b : Z),
       implb (Z.eqb a b) (Z.eqb (f (Some a)) (f (Some b))).
-  Proof. verit. auto with typeclass_instances. Qed.
+  Proof. verit. Qed.
 
   Goal forall (f : option Z -> Z) (a b : Z), a = b -> f (Some a) = f (Some b).
-  Proof. verit. auto with typeclass_instances. Qed.
+  Proof. verit. Qed.
 End AppliedPolymorphicTypes1.
 
 
-- 
cgit