diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 574088f420..71b054cd6e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -122,6 +122,8 @@ let rec subst_meta_instances bl c = (try pi2 (List.find select bl) with Not_found -> c) | _ -> map_constr (subst_meta_instances bl) c +(** [env] should be the context in which the metas live *) + let pose_all_metas_as_evars env evd t = let evdref = ref evd in let rec aux t = match kind_of_term t with @@ -143,14 +145,18 @@ let pose_all_metas_as_evars env evd t = let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = match kind_of_term f with | Meta k -> - let sigma,c = pose_all_metas_as_evars env sigma c in + (* We enforce that the Meta does not depend on the [nb] + extra assumptions added by unification to the context *) + let env' = pop_rel_context nb env in + let sigma,c = pose_all_metas_as_evars env' sigma c in let c = solve_pattern_eqn env l c in let pb = (Conv,TypeNotProcessed) in if noccur_between 1 nb c then sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst else error_cannot_unify_local env sigma (applist (f, l),c,c) | Evar ev -> - let sigma,c = pose_all_metas_as_evars env sigma c in + let env' = pop_rel_context nb env in + let sigma,c = pose_all_metas_as_evars env' sigma c in sigma,metasubst,(env,ev,solve_pattern_eqn env l c)::evarsubst | _ -> assert false |