From a80842f443b65d1bab4d9a4916017fc336f333fd Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 10 Sep 2010 13:37:24 +0000
Subject: Bugfix: A notation for a constructor where some arguments are _ is
 now allowed on the left side of a match.

You can write 'match v with |Vnil => 0 |h :: q => 1 end.' if
'h :: q' stands for the vector 'Vcons _ h _ t'.

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

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 04fe942a15..8bb240d6e9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -813,6 +813,7 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
 	  match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
+  | AHole _ -> ([],[[], PatVar (loc,Anonymous)])
   | t -> error_invalid_pattern_notation loc
   in aux alias fullsubst a
 
-- 
cgit v1.2.3