From 0ddfbbd940b47b133cfc9daf3c657a32c02e14ba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 Sep 2003 15:34:50 +0000
Subject: Syntaxe plus liberale pour le type des arguments de filtrage du
 'match'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constrnew.ml4 | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index c3a7c27b3a..e8f9c38c5e 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -287,9 +287,7 @@ GEXTEND Gram
   ;
   pred_pattern:
     [ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous];
-        ty = OPT ["in"; r=global; nal=LIST0 name ->
-          (loc,r,List.map snd nal)] ->
-          (oid,ty) ] ]
+        ty = OPT ["in"; t=lconstr -> t] -> (oid,ty) ] ]
   ;
   case_type:
     [ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ]
-- 
cgit v1.2.3