diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e8a0df484..b42a70b34 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1582,7 +1582,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in - if Context.eq_named_declaration d newdecl + if Context.Named.Declaration.equal d newdecl && not (indirectly_dependent c d depdecls) then if check_occs && not (in_every_hyp occs) @@ -1634,7 +1634,7 @@ type abstraction_request = type 'r abstraction_result = Names.Id.t * named_context_val * - Context.named_declaration list * Names.Id.t option * + Context.Named.Declaration.t list * Names.Id.t option * types * (constr, 'r) Sigma.sigma option let make_abstraction env evd ccl abs = |