diff options
| author | herbelin | 2011-11-16 08:46:26 +0000 |
|---|---|---|
| committer | herbelin | 2011-11-16 08:46:26 +0000 |
| commit | 2556a4bcfe9bbad8b3fe555997bb272102fec1dd (patch) | |
| tree | 411d1e3f2646a8d0f77a4ba1039ceaeb674e4836 | |
| parent | 96232cde20378e6527a940c6f94d3ad71f1c5ca3 (diff) | |
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
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |