From deb9927455bcb3b506d17a63a9b7b5ec11fe9027 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 14 Apr 2022 18:01:03 +0200
Subject: Port

---
 src/Tactics.v | 87 ++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 45 insertions(+), 42 deletions(-)

diff --git a/src/Tactics.v b/src/Tactics.v
index 727e0b7..6f2c7b1 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -94,30 +94,33 @@ Tactic Notation "verit_bool_no_check"           :=
   let Hs := get_hyps in
   fun Hs => verit_bool_no_check_base_auto Hs; vauto.
 
+
 (** Tactics in bool with timeout **)
 
 Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances.
 Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances.
 
 Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) :=
-  get_hyps ltac:(fun Hs =>
-                   match Hs with
-                   | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout
-                   | None => verit_bool_base_auto_timeout (Some h) timeout
-                   end;
-                   vauto).
+  let Hs := get_hyps in
+  match Hs with
+  | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout
+  | None => verit_bool_base_auto_timeout (Some h) timeout
+  end;
+  vauto.
 Tactic Notation "verit_bool_timeout"  int_or_var(timeout)         :=
-  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto).
+  let Hs := get_hyps in
+  verit_bool_base_auto_timeout Hs timeout; vauto.
 
 Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) :=
-  get_hyps ltac:(fun Hs =>
-                   match Hs with
-                   | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout
-                   | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
-                   end;
-                   vauto).
+  let Hs := get_hyps in
+  match Hs with
+  | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout
+  | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
+  end;
+  vauto.
 Tactic Notation "verit_bool_no_check_timeout"   int_or_var(timeout)        :=
-  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto).
+  let Hs := get_hyps in
+  verit_bool_no_check_base_auto_timeout Hs timeout; vauto.
 
 
 (** Tactics in Prop **)
@@ -173,46 +176,46 @@ Tactic Notation "verit_no_check"           :=
 Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
-         [ .. | get_hyps ltac:(fun Hs =>
-                                 match Hs with
-                                   | Some ?Hs =>
-                                     prop2bool_hyps Hs;
-                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout]
-                                   | None => verit_bool_base_auto_timeout (Some h) timeout
-                                 end; vauto)
+         [ .. | let Hs := get_hyps in
+                match Hs with
+                | Some ?Hs =>
+                    prop2bool_hyps Hs;
+                    [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout ]
+                | None => verit_bool_base_auto_timeout (Some h) timeout
+                end; vauto
          ]
   ].
 Tactic Notation "verit_timeout"   int_or_var(timeout)        :=
   prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          match Hs with
-                          | Some ?Hs =>
-                            prop2bool_hyps Hs;
-                            [ .. | verit_bool_base_auto_timeout (Some Hs) timeout]
-                          | None => verit_bool_base_auto_timeout (@None nat) timeout
-                          end; vauto)
+  [ .. | let Hs := get_hyps in
+         match Hs with
+         | Some ?Hs =>
+             prop2bool_hyps Hs;
+             [ .. | verit_bool_base_auto_timeout (Some Hs) timeout ]
+         | None => verit_bool_base_auto_timeout (@None nat) timeout
+         end; vauto
   ].
 Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
-         [ .. | get_hyps ltac:(fun Hs =>
-                                 match Hs with
-                                   | Some ?Hs =>
-                                     prop2bool_hyps Hs;
-                                     [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ]
-                                   | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
-                                 end; vauto)
+         [ .. | let Hs := get_hyps in
+                match Hs with
+                | Some ?Hs =>
+                    prop2bool_hyps Hs;
+                    [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ]
+                | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
+                end; vauto
          ]
   ].
 Tactic Notation "verit_no_check_timeout"   int_or_var(timeout)        :=
   prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          match Hs with
-                          | Some ?Hs =>
-                            prop2bool_hyps Hs;
-                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout]
-                          | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
-                          end; vauto)
+  [ .. | let Hs := get_hyps in
+         match Hs with
+         | Some ?Hs =>
+             prop2bool_hyps Hs;
+             [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout ]
+         | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
+         end; vauto
   ].
 
 
-- 
cgit