From a467cd39586159fa660e5f5dc557efaad03426c9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 27 Oct 2004 17:04:04 +0000
Subject: Bug mauvais nom d'entrée binder_constr quand récursion gauche

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

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 0f6951d476..081d7aeecc 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -774,7 +774,9 @@ let is_self from e =
 
 let is_binder_level from e =
   match from, e with
-      ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7
+      ETConstr(200,()),
+      ETConstr(NumLevel 200,(BorderProd(false,_)|InternalProd)) ->
+        not !Options.v7
     | _ -> false
 
 let rec symbol_of_production assoc from forpat typ =
@@ -799,5 +801,3 @@ let rec symbol_of_production assoc from forpat typ =
       | (eobj,Some None,_) -> Gramext.Snext
       | (eobj,Some (Some (lev,cur)),_) -> 
           Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level assoc cur lev)
-
-
-- 
cgit v1.2.3