diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 112402bca9..6873bbb112 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -107,8 +107,11 @@ let fail_quick_unif_flags = { let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = let env = pf_env gls in let evd = create_goal_evar_defs (project gls) in - let evd' = w_unify env evd CONV ~flags m n in - tclIDTAC {it = gls.it; sigma = evd'; } + try + let evd' = w_unify env evd CONV ~flags m n in + tclIDTAC {it = gls.it; sigma = evd'; } + with e when Errors.noncritical e -> + tclFAIL 0 (Errors.print e) gls let unify ?(flags=fail_quick_unif_flags) m gls = let n = pf_concl gls in unifyTerms ~flags m n gls |