diff options
author | 2011-12-05 17:16:34 +0000 | |
---|---|---|
committer | 2011-12-05 17:16:34 +0000 | |
commit | 223429a0fe7de02ab4e495529b795f5733d6dd32 (patch) | |
tree | 8f3cfc9a52cab7d4c6b7c9f94bb570d4d8956fae /pretyping/evarutil.ml | |
parent | 973eeb5d9698b3cef601c42948a0c0f83cb38de1 (diff) |
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
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r-- | pretyping/evarutil.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 57a6426ab..fecfff7a5 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 |