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

1 files changed, 5 insertions, 3 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 953d9559d9..6bcf226653 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