Permalink
Browse files

Add a try catch in case of failure

  • Loading branch information...
braibant committed Jan 24, 2013
1 parent 2ef1dc5 commit facaf2af1eedd3bd5760c7f57b5634e2254fd379
Showing with 9 additions and 5 deletions.
  1. +9 −5 src/evm_compute.ml4
View
@@ -184,18 +184,22 @@ let evm_compute eq blacklist = fun gl ->
mk_let (!! "t") t typeof_t (fun t -> let t' = Term.mkVar t in
mk_let (!! "H") (mk_vm_cast (Leibniz.eq typeof_t t' nft') (Leibniz.eq_refl typeof_t nft')) (Leibniz.eq typeof_t t' nft')
(fun h ->
- (* typeof_t -> Prop *)
+ (* typeof_t -> Prop *)
let body = Leibniz.eq_ind_r typeof_t
nft' p pnft t' (Term.mkVar h)
in
Term.mkCast (body, Term.DEFAULTcast, Term.mkApp (t', argsv))
)))
end in
- assert_tac "subgoal" (Term.mkApp (p,[| nft |]))
- (fun subgoal ->
- Tactics.exact_no_check (proof_term (Term.mkVar subgoal))
- ) gl
+ try
+ assert_tac "subgoal" (Term.mkApp (p,[| nft |]))
+ (fun subgoal ->
+ 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))
+
;;

0 comments on commit facaf2a

Please sign in to comment.