diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 99c20ef6ce..01e1154e58 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1780,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = try (* This is up to delta for subterms w/o metas ... *) w_unify_to_subterm env evd ~flags (strip_outer_cast op,t) - with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op) + with PretypeError (env,_,NoOccurrenceFound _) when + allow_K || + (* w_unify_to_subterm does not go through evars, so + the next step, which was already in <= 8.4, is + needed at least for compatibility of rewrite *) + dependent op t -> (evd,op) in if not allow_K && (* ensure we found a different instance *) |