diff options
| author |  amblaf <you@example.com> | 2017-07-12 15:44:37 +0200 |
|---|---|---|
| committer | amblaf <you@example.com> | 2017-07-31 10:34:05 +0200 |
| commit | 7ba6bc4554a642f78f59b996f99d9d6ca2cc2678 (patch) | |
| tree | 5781f1a0ed49b63b53312e0bed953380a2451052 /tactics/equality.ml | |
| parent | 1c10b84c0ce5f96a3afd1fc83c738c76070958c3 (diff) | |
better `try with` scope in `discr_positions`
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 6274bca9f..ad6abfa1f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1004,18 +1004,20 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_False () >>= fun false_0 -> let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - try - let discriminator = - build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath - in + let discriminator = + try + Proofview.tclUNIT + (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath) + with + UserError _ as ex -> Proofview.tclZERO ex + in + discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> let pf_ty = mkArrow eqn absurd_term in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous absurd_term) [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))] - with - UserError _ as ex -> Proofview.tclZERO ex let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in |