Correction d'un bug de l'unification pattern qui oubliait d'expanser

les alias avant de déclarer qu'une evar n'était appliquée qu'à des
variables.


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

4 files changed, 15 insertions, 11 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f4c19790d..e5edd6054 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -211,7 +211,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
 	  if 
-	    is_unification_pattern_evar ev1 l1 & 
+	    is_unification_pattern_evar env ev1 l1 & 
 	    not (occur_evar (fst ev1) (applist appr2))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
@@ -243,7 +243,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
 	  if 
-	    is_unification_pattern_evar ev2 l2 & 
+	    is_unification_pattern_evar env ev2 l2 & 
 	    not (occur_evar (fst ev2) (applist appr1))
 	  then
 	    (* Miller-Pfenning's patterns unification *)
@@ -302,7 +302,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, Rigid _ ->
 	if 
-	  is_unification_pattern_evar ev1 l1 & 
+	  is_unification_pattern_evar env ev1 l1 & 
 	  not (occur_evar (fst ev1) (applist appr2))
 	then
 	  (* Miller-Pfenning's patterns unification *)
@@ -317,7 +317,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Rigid _, Flexible ev2 ->
 	if 
-	  is_unification_pattern_evar ev2 l2 & 
+	  is_unification_pattern_evar env ev2 l2 & 
 	  not (occur_evar (fst ev2) (applist appr1))
 	then
 	  (* Miller-Pfenning's patterns unification *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 953d9559d..6bcf22665 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -982,20 +982,22 @@ let head_evar =
    that we don't care whether args itself contains Rel's or even Rel's
    distinct from the ones in l *)
 
-let is_unification_pattern_evar (_,args) l =
+let is_unification_pattern_evar env (_,args) l =
   let l' = Array.to_list args @ l in
+  let l' = List.map (expand_var env) l' in
   List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l'
 
-let is_unification_pattern f l =
+let is_unification_pattern env f l =
   match kind_of_term f with
     | Meta _ -> array_for_all isRel l & array_distinct l
-    | Evar ev -> is_unification_pattern_evar ev (Array.to_list l)
+    | Evar ev -> is_unification_pattern_evar env ev (Array.to_list l)
     | _ -> false
 
 (* From a unification problem "?X l1 = term1 l2" such that l1 is made
    of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
 
 let solve_pattern_eqn env l1 c =
+  let l1 = List.map (expand_var env) l1 in
   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
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 6540f8969..9a9d75eb8 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -88,8 +88,8 @@ val define_evar_as_product : evar_defs -> existential -> evar_defs * types
 val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
 val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
-val is_unification_pattern_evar : existential -> constr list -> bool
-val is_unification_pattern : constr -> constr array -> bool
+val is_unification_pattern_evar : env -> existential -> constr list -> bool
+val is_unification_pattern : env -> constr -> constr array -> bool
 val solve_pattern_eqn : env -> constr list -> constr -> constr
 
 (***********************************************************)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1063342e5..94468e6dc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -190,11 +190,13 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
 		  (unirec_rec curenv topconv true substn p1 p2) c1 c2) cl1 cl2
 
 	| App (f1,l1), _ when
-	    isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) ->
+	    isMeta f1 & is_unification_pattern curenv f1 l1 &
+	    not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenv f1 l1 cN substn
 
 	| _, App (f2,l2) when
-	    isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) ->
+	    isMeta f2 & is_unification_pattern curenv f2 l2 &
+	    not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenv f2 l2 cM substn
 
 	| App (f1,l1), App (f2,l2) ->