verit_timeout takes an integer as parameter

2 files changed, 26 insertions, 26 deletions

diff --git a/src/Tactics.v b/src/Tactics.v
index c44af14..316fcc1 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -91,28 +91,28 @@ Tactic Notation "verit_bool_no_check"           :=
 
 (** Tactics in bool with timeout **)
 
-Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances.
-Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances.
+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) :=
+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))
-                   | None => verit_bool_base_auto_timeout (Some h)
+                   | 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"           :=
-  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; vauto).
+Tactic Notation "verit_bool_timeout"  int_or_var(timeout)         :=
+  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto).
 
-Tactic Notation "verit_bool_no_check_timeout" constr(h) :=
+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))
-                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                   | 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"           :=
-  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; 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).
 
 
 (** Tactics in Prop **)
@@ -165,48 +165,48 @@ Tactic Notation "verit_no_check"           :=
                           end; vauto)
   ].
 
-Tactic Notation "verit_timeout" constr(h) :=
+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)) ]
-                                   | None => verit_bool_base_auto_timeout (Some h)
+                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout]
+                                   | None => verit_bool_base_auto_timeout (Some h) timeout
                                  end; vauto)
          ]
   ].
-Tactic Notation "verit_timeout"           :=
+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) ]
-                          | None => verit_bool_base_auto_timeout (@None nat)
+                            [ .. | 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) :=
+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)) ]
-                                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                                     [ .. | 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"           :=
+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) ]
-                          | None => verit_bool_no_check_base_auto_timeout (@None nat)
+                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout]
+                          | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
                           end; vauto)
   ].
 
diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg
index 19298f4..1d8f146 100644
--- a/src/g_smtcoq.mlg
+++ b/src/g_smtcoq.mlg
@@ -115,8 +115,8 @@ END
 TACTIC EXTEND Tactic_verit
 | [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) }
 | [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) }
-| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) }
-| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) }
+| [ "verit_bool_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic (Some timeout) lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic_no_check (Some timeout) lpl (get_lemmas ()) }
 END
 
 TACTIC EXTEND Tactic_cvc4