diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-20 20:02:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-20 20:02:39 +0000 |
| commit | 27a7627fe5f9b3d3715abb133229ebc446dd983b (patch) | |
| tree | 16eea57bba8b4348fdb5246a3c454fb04f8cd8f9 /pretyping/unification.ml | |
| parent | 49af62a75b55b86dd8e6fa22b55237444163d7c6 (diff) | |
Fixing bug #1918 (no occur-check in Meta unification was done yet!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11818 85f007b7-540e-0410-9357-904b9bb8a0f7
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 6c7ca8af2..102d918fb 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 |