diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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) |