More robust and uniform treatment of aliases in evarutil.ml

- Compute chain of aliases once for all so as to simplify code.
- In is_unification_pattern, expand all vars/rels of the unification
  problem until they are no longer vars/rels so that the list of
  vars/rels used in the rhs is correct, and, the list of arguments of
  the evars eventually become irreducible vars/rels (in particular,
  this solves bug #2615).
- Some points remain unclear, e.g. whether solve_evar_evar should
  reason with all let-in expanded or with let-in expanded only up
  to the last expansion which is still a var or rel.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14539 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 178 insertions, 136 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 121de57bf..ac6a574fc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -227,17 +227,17 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
-	  if
-	    is_unification_pattern_evar env ev1 l1 (applist appr2) &
-	    not (occur_evar (fst ev1) (applist appr2))
-	  then
+          match is_unification_pattern env term1 l1 (applist appr2) with
+          | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar evd (applist appr2) in
-	    let t2 = solve_pattern_eqn env l1 t2 in
+	    let t2 = solve_pattern_eqn env l1' t2 in
 	    solve_simple_eqn (evar_conv_x ts) env evd
 	      (position_problem true pbty,ev1,t2)
-	  else if
+          | None -> (i,false)
+        and f2 i =
+	  if
             List.length l1 <= List.length l2
 	  then
 	    (* Try first-order unification *)
@@ -250,27 +250,27 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                   (fun i -> evar_conv_x ts env i CONV) l1 rest2);
                (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
           else (i,false)
-	and f2 i =
+	and f3 i =
 	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2)
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f2]
+	ise_try evd [f1; f2; f3]
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
-	  if
-	    is_unification_pattern_evar env ev2 l2 (applist appr1) &
-	    not (occur_evar (fst ev2) (applist appr1))
-	  then
+	  match is_unification_pattern env term2 l2 (applist appr1) with
+          | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar evd (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
 	    solve_simple_eqn (evar_conv_x ts) env evd
 	      (position_problem false pbty,ev2,t1)
-	  else if
+          | None -> (i,false)
+        and f2 i =
+          if
        	    List.length l2 <= List.length l1
 	  then
 	    (* Try first-order unification *)
@@ -282,13 +282,13 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                   (fun i -> evar_conv_x ts env i CONV) rest1 l2);
                (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
           else (i,false)
-	and f2 i =
+	and f3 i =
 	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2
 	    | None -> (i,false)
 	in
-	ise_try evd [f1; f2]
+	ise_try evd [f1; f2; f3]
 
     | MaybeFlexible flex1, MaybeFlexible flex2 -> begin
         match kind_of_term flex1, kind_of_term flex2 with
@@ -358,36 +358,32 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, (Rigid _ | PseudoRigid _) ->
-	if
-	  is_unification_pattern_evar env ev1 l1 (applist appr2) &
-	  not (occur_evar (fst ev1) (applist appr2))
-	then
+	(match is_unification_pattern env term1 l1 (applist appr2) with
+        | Some l1 ->
 	  (* Miller-Pfenning's pattern unification *)
 	  (* Preserve generality thanks to eta-conversion) *)
 	  let t2 = nf_evar evd (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,ev1,t2)
-	else
+        | None ->
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
-	  true
+	  true)
 
     | (Rigid _ | PseudoRigid _), Flexible ev2 ->
-	if
-	  is_unification_pattern_evar env ev2 l2 (applist appr1) &
-	  not (occur_evar (fst ev2) (applist appr1))
-	then
+	(match is_unification_pattern env term2 l2 (applist appr1) with
+        | Some l2 ->
 	  (* Miller-Pfenning's pattern unification *)
 	  (* Preserve generality thanks to eta-conversion) *)
 	  let t1 = nf_evar evd (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,ev2,t1)
-	else
+        | None ->
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
-	  true
+	  true)
 
     | MaybeFlexible flex1, (Rigid _ | PseudoRigid _) ->
 	let f3 i =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 860a2c830..e9f8db47b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -166,74 +166,110 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter insta
    dependencies in variables are canonically associated to the most ancient
    variable in its family of aliased variables *)
 
-let compute_aliases sign =
+let compute_var_aliases sign =
   List.fold_right (fun (id,b,c) aliases ->
     match b with
     | Some t ->
-	(match kind_of_term t with
-	| Var id' ->
-	    let id'' = try Idmap.find id' aliases with Not_found -> id' in
-	    Idmap.add id id'' aliases
-	| _ -> aliases)
-    | None -> aliases) sign Idmap.empty
-
-let alias_of_var id aliases = try Idmap.find id aliases with Not_found -> id
+        let aliases_of_id = match kind_of_term t with
+	| Var id' -> (try Idmap.find id' aliases with Not_found -> [])
+	| _ -> [] in
+	Idmap.add id (aliases_of_id@[t]) aliases
+    | None -> aliases)
+    sign Idmap.empty
+
+let compute_rel_aliases var_aliases rels =
+  snd (List.fold_right (fun (_,b,t) (n,aliases) ->
+    (n-1,
+     match b with
+     | Some t ->
+         let aliases_of_n = match kind_of_term t with
+	 | Var id' -> (try Idmap.find id' var_aliases with Not_found -> [])
+         | Rel p -> (try Intmap.find (p+n) aliases with Not_found -> [])
+         | _ -> [] in
+	 Intmap.add n (aliases_of_n@[lift n t]) aliases
+     | None -> aliases))
+      rels (List.length rels,Intmap.empty))
 
 let make_alias_map env =
-  let var_aliases = compute_aliases (named_context env) in
-  let rels = rel_context env in
-  let rel_aliases = 
-    snd (List.fold_right (fun (_,b,t) (n,aliases) ->
-      (n-1,
-      match b with
-	| Some t when isRel t or isVar t -> Intmap.add n (lift n t) aliases
-	| _ -> aliases)) rels (List.length rels,Intmap.empty)) in
+  (* We compute the chain of aliases for each var and rel *)
+  let var_aliases = compute_var_aliases (named_context env) in
+  let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
   (var_aliases,rel_aliases)
 
-let expand_var_once aliases x = match kind_of_term x with
-  | Rel n -> Intmap.find n (snd aliases)
-  | Var id -> mkVar (Idmap.find id (fst aliases))
-  | _ -> raise Not_found
+let get_alias_chain_of aliases x = match kind_of_term x with
+  | Rel n -> (try Intmap.find n (snd aliases) with Not_found -> [])
+  | Var id -> (try Idmap.find id (fst aliases) with Not_found -> [])
+  | _ -> []
+
+let normalize_alias_opt aliases x =
+  match get_alias_chain_of aliases x with
+  | []  -> None
+  | a::_ when isRel a || isVar a -> Some a (* Oldest alias is var/rel *)
+  | [a] -> None       (* Only one alias but not to var/rel *)
+  | _::a::_ -> Some a (* Last alias not to var/rel, but penultimate must be ok*)
 
-let rec expand_var_at_least_once aliases x =
-  let t = expand_var_once aliases x in
-  try expand_var_at_least_once aliases t
-  with Not_found -> t
+let normalize_alias aliases x =
+  match normalize_alias_opt aliases x with
+  | Some x -> x
+  | None -> x
 
-let expand_var aliases x =
-  try expand_var_at_least_once aliases x with Not_found -> x
+let expand_alias aliases x =
+  match get_alias_chain_of aliases x with
+  | []  -> x
+  | a::_ -> x
 
-let expand_var_opt aliases x =
-  try Some (expand_var_at_least_once aliases x) with Not_found -> None
+let normalize_alias_var var_aliases id =
+  destVar (normalize_alias (var_aliases,Intmap.empty) (mkVar id))
 
 let extend_alias (_,b,_) (var_aliases,rel_aliases) =
   let rel_aliases =
-    Intmap.fold (fun n c -> Intmap.add (n+1) (lift 1 c))
+    Intmap.fold (fun n l -> Intmap.add (n+1) (List.map (lift 1) l))
       rel_aliases Intmap.empty in
   let rel_aliases =
     match b with
-    | Some t when isRel t or isVar t -> Intmap.add 1 (lift 1 t) rel_aliases
-    | _ -> rel_aliases in
+    | Some t ->
+        let aliases = match kind_of_term t with
+	| Var id' -> (try Idmap.find id' var_aliases with Not_found -> [])
+        | Rel p -> (try Intmap.find (p+1) rel_aliases with Not_found -> [])
+        | _ -> [] in 
+	Intmap.add 1 (aliases@[lift 1 t]) rel_aliases
+    | None -> rel_aliases in
   (var_aliases, rel_aliases)
 
+let rec expansions_of_var aliases x =
+  match get_alias_chain_of aliases x with
+  | a::l when not (isVar a or isRel a) -> x :: List.rev l
+  | l -> x :: List.rev l
+
 let rec expand_vars_in_term_using aliases t = match kind_of_term t with
   | Rel _ | Var _ ->
-      expand_var aliases t
+      normalize_alias aliases t
   | _ ->
       map_constr_with_full_binders
 	extend_alias expand_vars_in_term_using aliases t
 
 let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
-let rec expansions_of_var aliases x =
-  try
-    let t = expand_var_once aliases x in
-    t :: expansions_of_var aliases t
-  with Not_found ->
-    [x]
-
-let expand_full_opt aliases y =
-  try expand_var_opt aliases y with Not_found -> None
+let free_vars_and_rels_up_alias_expansion aliases c =
+  let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
+  let rec frec (aliases,depth) c = match kind_of_term c with
+    | Rel _ | Var _ ->
+      let c = expand_alias aliases c in
+        (match kind_of_term c with
+        | Var id -> acc2 := Idset.add id !acc2
+        | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
+        | _ -> 
+            (* not optimal: would need sharing if alias occurs more than once *)
+            frec (aliases,depth) c)
+    | Const _ | Ind _ | Construct _ ->
+        acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
+    | _ ->
+        iter_constr_with_full_binders
+          (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
+          frec (aliases,depth) c
+  in
+  frec (aliases,0) c;
+  (!acc1,!acc2)
 
 (* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
  * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
@@ -247,7 +283,7 @@ let expand_full_opt aliases y =
 
 let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
-  let evar_aliases = compute_aliases sign in
+  let evar_aliases = compute_var_aliases sign in
   let (_,full_subst,cstr_subst) =
     List.fold_right
       (fun (id,b,c) (args,all,cstrs) ->
@@ -261,21 +297,21 @@ let make_projectable_subst aliases sigma evi args =
 		  let l = try Constrmap.find cstr cstrs with Not_found -> [] in
 		  Constrmap.add cstr ((args,id)::l) cstrs
 	      | _ -> cstrs in
-	    (rest,Idmap.add id [a,expand_full_opt aliases a,id] all,cstrs)
+	    (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
 	| Some c, a::rest ->
 	    let a = whd_evar sigma a in
 	    (match kind_of_term c with
 	    | Var id' ->
-		let idc = alias_of_var id' evar_aliases in
+		let idc = normalize_alias_var evar_aliases id' in
 		let sub = try Idmap.find idc all with Not_found -> [] in
 		if List.exists (fun (c,_,_) -> eq_constr a c) sub then
 		  (rest,all,cstrs)
 		else
 		  (rest,
-		   Idmap.add idc ((a,expand_full_opt aliases a,id)::sub) all,
+		   Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
 		   cstrs)
 	    | _ ->
-		(rest,Idmap.add id [a,expand_full_opt aliases a,id] all,cstrs))
+		(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
 	| _ -> anomaly "Instance does not match its signature")
       sign (array_rev_to_list args,Idmap.empty,Constrmap.empty) in
   (full_subst,cstr_subst)
@@ -666,12 +702,12 @@ let rec assoc_up_to_alias sigma aliases y yc = function
 	if l <> [] then assoc_up_to_alias sigma aliases y yc l
 	else
 	  (* Last chance, we reason up to alias conversion *)
-	  match (if c == c' then cc else expand_full_opt aliases c') with
+	  match (if c == c' then cc else normalize_alias_opt aliases c') with
 	  | Some cc when eq_constr yc cc -> id
 	  | _ -> if eq_constr yc c then id else raise Not_found
 
 let rec find_projectable_vars with_evars aliases sigma y subst =
-  let yc = expand_var aliases y in
+  let yc = normalize_alias aliases y in
   let is_projectable idc idcl subst' =
     (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
     try
@@ -1249,18 +1285,14 @@ let whd_head_evar_stack sigma c =
 
 let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
-(* Check if an applied evar "?X[args] l" is a Miller's pattern; note
-   that we don't care whether args itself contains Rel's or even Rel's
-   distinct from the ones in l *)
-
-let rec expand_and_check_vars env = function
+let rec expand_and_check_vars aliases = function
   | [] -> []
   | a::l ->
       if isRel a or isVar a then
-	let l = expand_and_check_vars env l in
-	match expand_var_opt env a with
-	| None -> a :: l
-	| Some a' when isRel a' or isVar a' -> list_add_set a' l
+	let l = expand_and_check_vars aliases l in
+	match get_alias_chain_of aliases a with
+	| [] -> a :: l
+	| a'::_ when isRel a' or isVar a' -> a' :: l
 	| _ -> raise Exit
       else
 	raise Exit
@@ -1280,49 +1312,54 @@ let rec constr_list_distinct l =
     | [] -> true
   in loop l
 
-let is_unification_pattern_evar env (_,args) l t =
-  List.for_all (fun x -> isRel x || isVar x) l (* common failure case *)
-  &&
+let get_actual_deps aliases l t =
+  if occur_meta_or_existential t then
+    (* Probably no restrictions on allowed vars in presence of evars *)
+    l
+  else
+    (* Probably strong restrictions coming from t being evar-closed *)
+    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    List.filter (fun c ->
+      match kind_of_term c with
+      | Var id -> Idset.mem id fv_ids
+      | Rel n -> Intset.mem n fv_rels
+      | _ -> assert false) l
+
+(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
+
+let find_unification_pattern_args env args l t =
+  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
     let aliases = make_alias_map env in
     let l' = Array.to_list args @ l in
-    let l'' = try Some (expand_and_check_vars aliases l') with Exit -> None in
-    match l'' with
-    | Some l ->
-	let deps =
-	  if occur_meta_or_existential t then
-	    (* Probably no restrictions on allowed vars in presence of evars *)
-	    l
-	  else
-	    (* Probably strong restrictions coming from t being evar-closed *)
-	    let t = expand_vars_in_term_using aliases t in
-	    let fv_rels = free_rels t in
-	    let fv_ids = global_vars env t in
-	    List.filter (fun c ->
-	      match kind_of_term c with
-	      | Var id -> List.mem id fv_ids
-	      | Rel n -> Intset.mem n fv_rels
-	      | _ -> assert false) l in
-	constr_list_distinct deps
-    | None -> false
-
-let is_unification_pattern (env,nb) f l t =
+    match (try Some (expand_and_check_vars aliases l') with Exit -> None) with
+    | Some l when constr_list_distinct (get_actual_deps aliases l t) ->
+        Some (list_skipn (Array.length args) l)
+    | _ ->
+      None
+  else
+    None
+
+let is_unification_pattern env f l t =
   match kind_of_term f with
-    | Meta _ ->
-	let dummy_ev = (f,[||]) in
-	is_unification_pattern_evar env dummy_ev (Array.to_list l) t
-    | Evar ev ->
-	is_unification_pattern_evar env ev (Array.to_list l) t
+    | Meta m ->
+        (match find_unification_pattern_args env [||] l t with
+        | Some _ as x when not (dependent f t) -> x
+        | _ -> None)
+    | Evar (evk,args) ->
+        (match find_unification_pattern_args env args l t with
+        | Some _ as x when not (occur_evar evk t) -> x
+        | _ -> None)
     | _ ->
-	false
+	None
 
-(* From a unification problem "?X l1 = term1 l2" such that l1 is made
-   of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
-(* NB: does not work when (term1 l2) contains metas because metas
+(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
+   (pattern unification). It is assumed that l is made of rel's that
+   are distinct and not bound to aliases. *)
+(* It is also assumed that c does not contain metas because metas
    *implicitly* depend on Vars but lambda abstraction will not reflect this
    dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
-let solve_pattern_eqn env l1 c =
-  let l1 = List.map (expand_var (make_alias_map env)) l1 in
+let solve_pattern_eqn env l c =
   let c' = List.fold_right (fun a c ->
     let c' = subst_term (lift 1 a) (lift 1 c) in
     match kind_of_term a with
@@ -1330,7 +1367,7 @@ let solve_pattern_eqn env l1 c =
       | Rel n -> let (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c')
       | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c'
       | _ -> assert false)
-    l1 c in
+    l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
      is not in normal form *)
   whd_eta c'
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d5f70b08d..365276853 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -96,10 +96,8 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
 
-val is_unification_pattern_evar : env -> existential -> constr list ->
-  constr -> bool
-val is_unification_pattern : env * int -> constr -> constr array ->
-  constr -> bool
+val is_unification_pattern : env -> constr -> constr list ->
+  constr -> constr list option
 
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
   evar_map * existential
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4a873f1f9..f1fdde390 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -112,18 +112,30 @@ 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 c = solve_pattern_eqn env (Array.to_list l) c 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 (mkApp (f, l),c,c)
+	  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
-	sigma,metasubst,(env,ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
+	sigma,metasubst,(env,ev,solve_pattern_eqn env l c)::evarsubst
     | _ -> assert false
 
 let push d (env,n) = (push_rel_assum d env,n+1)
 
+(* Hack to propagate data from an ocaml when clause to the actual branch code *)
+(* of a pattern-matching clause *)
+
+let whenmem = ref []
+
+let store mem = function
+  | Some l -> whenmem := l; true
+  | None -> false
+
+let restore mem = !mem
+
 (*******************************)
 
 (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -415,18 +427,16 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	       reduce curenvnb pb b substn cM cN)
 
 	| App (f1,l1), _ when
-	    (isMeta f1 && use_metas_pattern_unification flags (snd curenvnb) l1
+	    (isMeta f1 && use_metas_pattern_unification flags nb l1
              || use_evars_pattern_unification flags && isAllowedEvar flags f1) &
-	    is_unification_pattern curenvnb f1 l1 cN &
-	    not (dependent f1 cN) ->
-	      solve_pattern_eqn_array curenvnb f1 l1 cN substn
+	    store whenmem (is_unification_pattern curenv f1 (Array.to_list l1) cN) ->
+	      solve_pattern_eqn_array curenvnb f1 (restore whenmem) cN substn
 
 	| _, App (f2,l2) when
-	    (isMeta f2 && use_metas_pattern_unification flags (snd curenvnb) l2
+	    (isMeta f2 && use_metas_pattern_unification flags nb l2
              || use_evars_pattern_unification flags && isAllowedEvar flags f2) &
-	    is_unification_pattern curenvnb f2 l2 cM &
-	    not (dependent f2 cM) ->
-	      solve_pattern_eqn_array curenvnb f2 l2 cM substn
+	    store whenmem (is_unification_pattern curenv f2 (Array.to_list l2) cM) ->
+	      solve_pattern_eqn_array curenvnb f2 (restore whenmem) cM substn
 
 	| App (f1,l1), App (f2,l2) ->
 	    let len1 = Array.length l1
@@ -461,6 +471,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		    match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
 		    expand curenvnb pb b substn cM f1 l1 cN f2 l2
 
+
   and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN =
     if use_full_betaiota flags && not (subterm_restriction b flags) then
       let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in