From f654e2f4a6741cd8697dc495a63108dad7496c88 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Feb 2003 22:27:58 +0000
Subject: Test de non bouclage malencontreux dans les niveaux

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3679 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index d0893107a7..d41ce28036 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -529,6 +529,8 @@ let rec merge_entry_types etyps' = function
 let set_entry_type etyps (x,typ) =
   let typ = try 
     match List.assoc x etyps, typ with
+      | _, (_,BorderProd (true,_)) ->
+	  error "The level of the leftmost non-terminal cannot be changed"
       | ETConstr (n,()), (_,BorderProd (left,_)) ->
           ETConstr (n,BorderProd (left,None))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
-- 
cgit v1.2.3