diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/cctac.ml | 16 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 28 |
3 files changed, 29 insertions, 19 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 06c9f87935..c12dd47990 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -247,6 +247,7 @@ let _M =mkMeta let rec proof_tac p : unit Proofview.tactic = Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> + try (* type_of can raise exceptions *) match p.p_rule with Ax c -> Proofview.V82.tactic (exact_check c) | SymAx c -> @@ -313,6 +314,7 @@ let rec proof_tac p : unit Proofview.tactic = let injt= mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e let refute_tac c t1 t2 p = let tt1=constr_of_term t1 and tt2=constr_of_term t2 in @@ -454,12 +456,14 @@ let f_equal = Proofview.Goal.concl >>= fun concl -> Tacmach.New.pf_apply Typing.type_of >>= fun type_of -> let cut_eq c1 c2 = - let ty = Termops.refresh_universes (type_of c1) in - Proofview.V82.tactic begin - tclTHENTRY - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (simple_reflexivity ()) - end + try (* type_of can raise an exception *) + let ty = Termops.refresh_universes (type_of c1) in + Proofview.V82.tactic begin + tclTHENTRY + (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) + (simple_reflexivity ()) + end + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match kind_of_term concl with diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 70c6d22121..865fb386a8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1782,7 +1782,9 @@ let destructure_hyps = end in Proofview.Goal.hyps >>= fun hyps -> - loop (Environ.named_context_of_val hyps) + try (* type_of can raise exceptions *) + loop (Environ.named_context_of_val hyps) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e let destructure_goal = Proofview.Goal.concl >>= fun concl -> diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 010a550f0c..7bd0c7e43d 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -800,12 +800,14 @@ open Proofview.Notations let ring_lookup (f:glob_tactic_expr) lH rl t = Proofview.tclEVARMAP >= fun sigma -> Proofview.Goal.env >>= fun env -> - let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list e.ring_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let ring = ltac_ring_structure e in - ltac_apply f (ring@[lH;rl]) + try (* find_ring_strucure can raise an exception *) + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl in + let rl = carg (make_term_list e.ring_carrier rl) in + let lH = carg (make_hyp_list env lH) in + let ring = ltac_ring_structure e in + ltac_apply f (ring@[lH;rl]) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> @@ -1121,12 +1123,14 @@ let ltac_field_structure e = let field_lookup (f:glob_tactic_expr) lH rl t = Proofview.tclEVARMAP >= fun sigma -> Proofview.Goal.env >>= fun env -> - let rl = make_args_list rl t in - let e = find_field_structure env sigma rl in - let rl = carg (make_term_list e.field_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let field = ltac_field_structure e in - ltac_apply f (field@[lH;rl]) + try + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl in + let rl = carg (make_term_list e.field_carrier rl) in + let lH = carg (make_hyp_list env lH) in + let field = ltac_field_structure e in + ltac_apply f (field@[lH;rl]) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e TACTIC EXTEND field_lookup |