Yet another fix about alias in testing if pattern unification applies.

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

1 files changed, 6 insertions, 5 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 57a6426abe..fecfff7a58 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1299,11 +1299,12 @@ let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
 let rec expand_and_check_vars aliases = function
   | [] -> []
-  | a::l ->
-      if isRel a or isVar a then
-        normalize_alias aliases a :: expand_and_check_vars aliases l
-      else
-	raise Exit
+  | a::l when isRel a or isVar a ->
+      let a = expansion_of_var aliases a in
+      if isRel a or isVar a then a :: expand_and_check_vars aliases l
+      else raise Exit
+  | _ ->
+      raise Exit
 
 module Constrhash = Hashtbl.Make
   (struct type t = constr