Merge remote-tracking branch 'origin/coq-8.11' into timeout_verit

1 files changed, 66 insertions, 61 deletions

diff --git a/src/Tactics.v b/src/Tactics.v
index 316fcc1..727e0b7 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -1,7 +1,7 @@
 (**************************************************************************)
 (*                                                                        *)
 (*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
+(*     Copyright (C) 2011 - 2022                                          *)
 (*                                                                        *)
 (*     See file "AUTHORS" for the list of authors                         *)
 (*                                                                        *)
@@ -19,7 +19,7 @@ Declare ML Module "smtcoq_plugin".
 
 (** Collect all the hypotheses from the context *)
 
-Ltac get_hyps_acc acc k :=
+Ltac get_hyps_acc acc :=
   match goal with
   | [ H : ?P |- _ ] =>
     let T := type of P in
@@ -28,15 +28,15 @@ Ltac get_hyps_acc acc k :=
       lazymatch P with
       | id _ => fail
       | _ =>
-        change P with (id P) in H;
+        let _ := match goal with _ => change P with (id P) in H end in
         lazymatch acc with
-        | Some ?t => get_hyps_acc (Some (H, t)) k
-        | None => get_hyps_acc (Some H) k
+        | Some ?t => get_hyps_acc (Some (H, t))
+        | None => get_hyps_acc (Some H)
         end
       end
     | _ => fail
     end
-  | _ => k acc
+  | _ => acc
   end.
 
 Ltac eliminate_id :=
@@ -48,46 +48,51 @@ Ltac eliminate_id :=
     end
   end.
 
-Ltac get_hyps k := get_hyps_acc (@None nat) ltac:(fun Hs => eliminate_id; k Hs).
+Ltac get_hyps :=
+  let Hs := get_hyps_acc (@None nat) in
+  let _ := match goal with _ => eliminate_id end in
+  Hs.
 
 
-Section Test.
-  Variable A : Type.
-  Hypothesis H1 : forall a:A, a = a.
-  Variable n : Z.
-  Hypothesis H2 : n = 17%Z.
+(* Section Test. *)
+(*   Variable A : Type. *)
+(*   Hypothesis H1 : forall a:A, a = a. *)
+(*   Variable n : Z. *)
+(*   Hypothesis H2 : n = 17%Z. *)
 
-  Goal True.
-  Proof.
-    (* get_hyps ltac:(fun acc => idtac acc). *)
-  Abort.
-End Test.
+(*   Goal True. *)
+(*   Proof. *)
+(*     let Hs := get_hyps in idtac Hs. *)
+(*   Abort. *)
+(* 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_base_auto" constr(h) := verit_bool_base h; try (exact _).
+Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; try (exact _).
 
 Tactic Notation "verit_bool" constr(h) :=
-  get_hyps ltac:(fun Hs =>
-                   match Hs with
-                   | Some ?Hs => verit_bool_base_auto (Some (h, Hs))
-                   | None => verit_bool_base_auto (Some h)
-                   end;
-                   vauto).
+  let Hs := get_hyps in
+  match Hs with
+  | 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_auto Hs; vauto).
+  let Hs := get_hyps in
+  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_auto (Some (h, Hs))
-                   | None => verit_bool_no_check_base_auto (Some h)
-                   end;
-                   vauto).
+  let Hs := get_hyps in
+  match Hs with
+  | 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_auto Hs; vauto).
+  let Hs := get_hyps in
+  fun Hs => verit_bool_no_check_base_auto Hs; vauto.
 
 (** Tactics in bool with timeout **)
 
@@ -123,46 +128,46 @@ Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop.
 Tactic Notation "verit" constr(h) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
-         [ .. | get_hyps ltac:(fun Hs =>
-                                 match Hs with
-                                   | Some ?Hs =>
-                                     prop2bool_hyps Hs;
-                                     [ .. | verit_bool_base_auto (Some (h, Hs)) ]
-                                   | None => verit_bool_base_auto (Some h)
-                                 end; vauto)
+         [ .. | let Hs := get_hyps in
+                match Hs with
+                | Some ?Hs =>
+                  prop2bool_hyps Hs;
+                  [ .. | verit_bool_base_auto (Some (h, Hs)) ]
+                | None => verit_bool_base_auto (Some h)
+                end; vauto
          ]
   ].
 Tactic Notation "verit"           :=
   prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          match Hs with
-                          | Some ?Hs =>
-                            prop2bool_hyps Hs;
-                            [ .. | verit_bool_base_auto (Some Hs) ]
-                          | None => verit_bool_base_auto (@None nat)
-                          end; vauto)
+  [ .. | let Hs := get_hyps in
+         match Hs with
+         | Some ?Hs =>
+           prop2bool_hyps Hs;
+           [ .. | verit_bool_base_auto (Some Hs) ]
+         | None => verit_bool_base_auto (@None nat)
+         end; vauto
   ].
 Tactic Notation "verit_no_check" constr(h) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
-         [ .. | get_hyps ltac:(fun Hs =>
-                                 match Hs with
-                                   | Some ?Hs =>
-                                     prop2bool_hyps Hs;
-                                     [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ]
-                                   | None => verit_bool_no_check_base_auto (Some h)
-                                 end; vauto)
+         [ .. | let Hs := get_hyps in
+                match Hs with
+                | Some ?Hs =>
+                  prop2bool_hyps Hs;
+                  [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ]
+                | None => verit_bool_no_check_base_auto (Some h)
+                end; vauto
          ]
   ].
 Tactic Notation "verit_no_check"           :=
   prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          match Hs with
-                          | Some ?Hs =>
-                            prop2bool_hyps Hs;
-                            [ .. | verit_bool_no_check_base_auto (Some Hs) ]
-                          | None => verit_bool_no_check_base_auto (@None nat)
-                          end; vauto)
+  [ .. | let Hs := get_hyps in
+         match Hs with
+         | Some ?Hs =>
+           prop2bool_hyps Hs;
+           [ .. | verit_bool_no_check_base_auto (Some Hs) ]
+         | None => verit_bool_no_check_base_auto (@None nat)
+         end; vauto
   ].
 
 Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) :=