Skip to content
Browse files

Fail rather than raising an anomaly

  • Loading branch information...
1 parent facaf2a commit c71041c44a5679c9db3e685f117d50dba454c350 @braibant committed Jan 24, 2013
Showing with 4 additions and 2 deletions.
  1. +1 −0 .gitignore
  2. +2 −1 src/evm_compute.ml4
  3. +1 −1 test-suite/Example.v
View
1 .gitignore
@@ -13,3 +13,4 @@
*.ml.d
*.o
Makefile-localvars.gen
+Makefile.coq
View
3 src/evm_compute.ml4
@@ -198,7 +198,8 @@ let evm_compute eq blacklist = fun gl ->
Tactics.exact_no_check (proof_term (Term.mkVar subgoal))
) gl
with
- | e -> Util.anomaly (Printf.sprintf "evm_compute failed with an exception %s" (Printexc.to_string e))
+ | e ->
+ Tacticals.tclFAIL 0 (Pp.str (Printf.sprintf "evm_compute failed with an exception %s" (Printexc.to_string e))) gl
;;
View
2 test-suite/Example.v
@@ -80,7 +80,7 @@ intros. eexists. eexists.
rewrite <- factorisable.
evm blacklist [Zmult].
unfold H, H0. reflexivity.
-Show Proof. Time Qed.
+Qed.

0 comments on commit c71041c

Please sign in to comment.
Something went wrong with that request. Please try again.