From 5f3f8ae162a4248ed5a12929793735d967dd869d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 22 Aug 2007 11:45:09 +0000
Subject: - Correction bug dans syntaxe des match (liste de motifs vide était
 acceptée) - Des open en plus dans le débogueur-traceur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10083 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include     | 3 ++-
 parsing/g_constr.ml4 | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/dev/base_include b/dev/base_include
index 26949cde98..829c5ea61c 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -64,9 +64,10 @@ open Pattern
 open Cbv
 open Classops
 open Pretyping
+open Pretyping.Default
+open Pretyping.Default.Cases
 open Cbv
 open Classops
-open Pretyping
 open Clenv
 open Rawterm
 open Coercion
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5e68c73089..10d7f46b57 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -275,7 +275,7 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   eqn:
-    [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; 
+    [ [ pll = LIST1 LIST1 pattern LEVEL "99" SEP "," SEP "|"; 
         "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
   ;
   pattern:
-- 
cgit v1.2.3