verit_timeout takes an integer as parameter

2 files changed, 22 insertions, 29 deletions

diff --git a/examples/Example.v b/examples/Example.v
index b949740..9fcb555 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -14,7 +14,6 @@
    If you are using native-coq instead of Coq 8.11, replace it with:
      Require Import SMTCoq.
    *)
-
 Require Import SMTCoq.SMTCoq.
 Require Import Bool.
 
@@ -425,3 +424,25 @@ Section CompCert.
   Qed.
 
 End CompCert.
+
+
+(** The verit solver can be called with an integer (the timeout in seconds).
+If the goal cannot be solved within timeout seconds, then an anomaly is raised **)
+
+Section test_timeout.
+
+Variable P : Z -> bool.
+Variable H0 : P 0.
+Variable HInd : forall n, implb (P n) (P (n + 1)).
+
+Goal P 3.
+(* verit_timeout 3. *) verit.
+Qed.
+
+Goal true -> P 1000000000.
+intro H.
+(* Fail verit_timeout 1. 
+Fail verit_timeout 5. *)
+Abort.
+
+End test_timeout.
diff --git a/examples/foo.v b/examples/foo.v
deleted file mode 100644
index c2162df..0000000
--- a/examples/foo.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Add Rec LoadPath "../src" as SMTCoq.
-Require Import SMTCoq.SMTCoq.
-Require Import ZArith.
-
-Section test_timeout.
-
-Variable P : Z -> bool.
-Variable H0 : P 0.
-Variable HInd : forall n, implb (P n) (P (n + 1)).
-
-Goal P 3.
-verit.
-Qed.
-
-Tactic Notation "verit_timeout2"           :=
-  prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          lazymatch Hs with
-                          | Some ?Hs => idtac 1 ;
-                            prop2bool_hyps Hs; idtac 2 ;
-                            [ .. | idtac 3 ; verit_bool_base_auto_timeout (Some Hs) ]
-                          | None => idtac 4 ; verit_bool_base_auto_timeout (@None nat)
-                          end)
-  ].
-
-Goal true -> P 1000000000.
-intro H.
-verit_timeout2. constructor.
\ No newline at end of file