use of anomaly for timeout

3 files changed, 7 insertions, 7 deletions

diff --git a/src/PropToBool.v b/src/PropToBool.v
index bbe1967..e06b336 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -164,10 +164,10 @@ Ltac prop2bool_hyp H :=
     destruct HFalse
   | ];
   clear H';
-  match (eval compute in prop2bool_comp) with
+  lazymatch (eval compute in prop2bool_comp) with
   | true =>
     let A := eval cbv in prop2bool_t in
-    match goal with
+    lazymatch goal with
     | [ _ : CompDec A |- _ ] => idtac
     | _ =>
       let Hcompdec := fresh "Hcompdec" in
@@ -195,7 +195,7 @@ Ltac prop2bool_hyp H :=
           | _ => prop2bool
           end in
       tac_rec;
-      match goal with
+      lazymatch goal with
       | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g
       end;
       destruct HFalse
@@ -213,9 +213,9 @@ Ltac prop2bool_hyp H :=
 
 Ltac remove_compdec_hyp H :=
   let TH := type of H in
-  match TH with
+  lazymatch TH with
   | forall p : CompDec ?A, _ =>
-    match goal with
+    lazymatch goal with
     | [ p' : CompDec A |- _ ] =>
       let H1 := fresh in
       assert (H1 := H p'); clear H; assert (H := H1); clear H1;
diff --git a/src/Tactics.v b/src/Tactics.v
index e41b0f5..c44af14 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -29,7 +29,7 @@ Ltac get_hyps_acc acc k :=
       | id _ => fail
       | _ =>
         change P with (id P) in H;
-        match acc with
+        lazymatch acc with
         | Some ?t => get_hyps_acc (Some (H, t)) k
         | None => get_hyps_acc (Some H) k
         end
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index b0c75a7..12efcc9 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -207,7 +207,7 @@ let call_verit timeout _ rt ro ra_quant rf_quant first lsmt =
           CoqInterface.error ("veriT failed with the error: " ^ l)
       done
     with End_of_file -> () in
-  if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = failwith "veriT timed out" in ());
+  if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = CErrors.anomaly (Pp.str "veriT timed out") in ()) ;
   try
     if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
     raise_warnings_errors ();