From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- tactics/equality.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'tactics/equality.ml') diff --git a/tactics/equality.ml b/tactics/equality.ml index a352355b..1c5e4b2f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -334,7 +334,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac try rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl - with e -> (* Try to see if there's an equality hidden *) + with e when Errors.noncritical e -> + (* Try to see if there's an equality hidden *) let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) match match_with_equality_type t' with @@ -1156,7 +1157,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = ] (* not a dep eq or no decidable type found *) ) else (raise Not_dep_pair) - ) with _ -> + ) with e when Errors.noncritical e -> inject_at_positions env sigma u eq_clause posns (fun _ -> intros_pattern no_move ipats) -- cgit v1.2.3