From 223429a0fe7de02ab4e495529b795f5733d6dd32 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Dec 2011 17:16:34 +0000
Subject: 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
---
 pretyping/evarutil.ml | 11 ++++++-----
 1 file 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
-- 
cgit v1.2.3