diff options
Diffstat (limited to 'pretyping')
| -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 6c7ca8af2c..102d918fb7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -190,7 +190,7 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = then (k1,cN,stN)::metasubst,evarsubst else if k1 = k2 then substn else (k2,cM,stM)::metasubst,evarsubst - | Meta k, _ -> + | Meta k, _ when not (dependent cM cN) -> (* Here we check that [cN] does not contain any local variables *) if nb = 0 then (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -198,7 +198,7 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst, evarsubst else error_cannot_unify_local curenv sigma (m,n,cN) - | _, Meta k -> + | _, Meta k when not (dependent cN cM) -> (* Here we check that [cM] does not contain any local variables *) if nb = 0 then (k,cM,snd (extract_instance_status pb))::metasubst,evarsubst |