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

2 files changed, 16 insertions, 13 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index daa0701b08..4bb9a9a5dc 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -649,11 +649,11 @@ let whd_meta metasubst c = match kind_of_term c with
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
 let plain_instance s c = 
-  let rec irec u = match kind_of_term u with
-    | Meta p -> (try List.assoc p s with Not_found -> u)
+  let rec irec n u = match kind_of_term u with
+    | Meta p -> (try lift n (List.assoc p s) with Not_found -> u)
     | App (f,l) when isCast f ->
         let (f,_,t) = destCast f in
-        let l' = Array.map irec l in 
+        let l' = Array.map (irec n) l in 
         (match kind_of_term f with
         | Meta p ->
 	    (* Don't flatten application nodes: this is used to extract a
@@ -666,12 +666,13 @@ let plain_instance s c =
                 mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
-        | _ -> mkApp (irec f,l'))	
+        | _ -> mkApp (irec n f,l'))	
     | Cast (m,_,_) when isMeta m ->
-	(try List.assoc (destMeta m) s with Not_found -> u)
-    | _ -> map_constr irec u
+	(try lift n (List.assoc (destMeta m) s) with Not_found -> u)
+    | _ ->
+	map_constr_with_binders succ irec n u
   in 
-  if s = [] then c else irec c
+  if s = [] then c else irec 0 c
 
 (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
    has (unfortunately) different subtle side effects: 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f0153b7910..f7762afbeb 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