From 2556a4bcfe9bbad8b3fe555997bb272102fec1dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 Nov 2011 08:46:26 +0000
Subject: Fixing association of wrong "as"-pattern name when expanding
 abbreviations of notations (most of the time inoffensive but has bad effect
 on compiling pattern-matching in the presence of dependencies).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14653 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7db10d81c6..8dee1f0e0f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -904,7 +904,7 @@ let find_constructor ref f aliases pats env =
 	   if List.length pats < nvars then error_not_enough_arguments loc;
 	   let pats1,pats2 = list_chop nvars pats in
 	   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
-	   let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) env) args in
+	   let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in
 	   cstr, idspl1, pats2
        | _ -> raise Not_found)
 
-- 
cgit v1.2.3