diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-04 18:38:23 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-04 18:38:23 +0000 |
| commit | a282e9f8d18b1dcf9dd46900b0af522f8e46d8ef (patch) | |
| tree | 3aced50383306e899f27a44fb57e79478735aef9 /pretyping/unification.ml | |
| parent | 44c3d5dfdf11a3fc948006e7da2ca70e9cd77357 (diff) | |
Fixes for unification and substitution of metas under binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f0153b791..f7762afbe 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -86,13 +86,15 @@ let rec subst_meta_instances bl c = | Meta i -> (try assoc_pair i bl with Not_found -> c) | _ -> map_constr (subst_meta_instances bl) c -let solve_pattern_eqn_array env f l c (metasubst,evarsubst) = +let solve_pattern_eqn_array (env,nb) sigma f l c (metasubst,evarsubst) = match kind_of_term f with | Meta k -> let c = solve_pattern_eqn env (Array.to_list l) c in let n = Array.length l - List.length (fst (decompose_lam c)) in let pb = (ConvUpToEta n,TypeNotProcessed) in - (k,c,pb)::metasubst,evarsubst + if noccur_between 1 nb c then + (k,lift (-nb) c,pb)::metasubst,evarsubst + else error_cannot_unify_local env sigma (mkApp (f, l),c,c) | Evar ev -> (* Currently unused: incompatible with eauto/eassumption backtracking *) metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst @@ -192,7 +194,7 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = (* Here we check that [cN] does not contain any local variables *) if nb = 0 then (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst - else if noccurn nb cN then + else if noccur_between 1 nb cN then (k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst, evarsubst else error_cannot_unify_local curenv sigma (m,n,cN) @@ -200,7 +202,7 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = (* Here we check that [cM] does not contain any local variables *) if nb = 0 then (k,cM,snd (extract_instance_status pb))::metasubst,evarsubst - else if noccurn nb cM + else if noccur_between 1 nb cM then (k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst, evarsubst @@ -224,12 +226,12 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = | App (f1,l1), _ when isMeta f1 & is_unification_pattern curenv f1 l1 & not (dependent f1 cN) -> - solve_pattern_eqn_array curenv f1 l1 cN substn + solve_pattern_eqn_array curenvnb sigma f1 l1 cN substn | _, App (f2,l2) when isMeta f2 & is_unification_pattern curenv f2 l2 & not (dependent f2 cM) -> - solve_pattern_eqn_array curenv f2 l2 cM substn + solve_pattern_eqn_array curenvnb sigma f2 l2 cM substn | App (f1,l1), App (f2,l2) -> let len1 = Array.length l1 |