Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a

un problème dû à la non réversibilité de la suppression de règles
camlp4 vis à vis de l'insertion : lorsqu'un niveau existant vide est
étendu, la suppression non seulement efface l'extension mais aussi le
niveau lui-même. Ceci a un effet sur les niveaux vides 8 et 99. Nous
n'avons pas trouvé de bonne solution à ce problème et l'utilisation
d'extensions aux niveaux 99 ou 8 (anciennement 5 avant ce commit)
continue de corrompre le parser si effectuées à l'intérieur de section
ou de modules. Voici un exemple montrant le problème :

Print Grammar constr. (* le niveau "8" existe *)
Section A.
Notation "{{ x }}" := (S x) (at level 8).
End A.
Print Grammar constr. (* le niveau "8" n'existe plus *)
Goal True. 
apply I.  (* appelle le niveau constr qui continue d'appeler "8"... échec *)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9756 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 19 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index 8c9a2e7bd..7a54ecf61 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,8 +8,7 @@ Commands
 
 Notations
 
-- Level "constr" moved from 9 to 5. User notations from levels 6 to 9
-  may have to be put at levels below 5 to be used without parentheses.
+- Level "constr" moved from 9 to 8.
 
 Tactic Language
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f2316ec5e..821426a3c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -131,7 +131,7 @@ GEXTEND Gram
     [ [ c = operconstr LEVEL "200" -> c ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "5" -> c ] ]
+    [ [ c = operconstr LEVEL "8" -> c ] ]
   ;
   operconstr:
     [ "200" RIGHTA
@@ -160,7 +160,7 @@ GEXTEND Gram
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
           CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
-    | "5" LEFTA [ ]
+    | "8" LEFTA [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 8f23c0f30..68659bb3e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -45,10 +45,19 @@ module L =
 
 module G = Grammar.Make(L)
 
-let grammar_delete e rls =
+let grammar_delete e pos rls =
   List.iter
-    (fun (_,_,lev) ->
-       List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+    (fun (n,ass,lev) ->
+
+      (* Caveat: deletion is not the converse of extension: when an
+	 empty level is extended, deletion removes the level instead
+	 of keeping it empty. This has an effect on the empty levels 8
+	 and 99. We didn't find a good solution to this problem
+	 (e.g. using G.extend to know if the level exists results in a
+	 printed error message as side effect). As a consequence an
+	 extension at 99 or 8 inside a section corrupts the parser. *)
+
+      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
     (List.rev rls)
 
 (* grammar_object is the superclass of all grammar entries *)
@@ -107,7 +116,7 @@ module Gram =
     include G
     let extend e pos rls =
       camlp4_state :=
-      (ByGEXTEND ((fun () -> grammar_delete e rls),
+      (ByGEXTEND ((fun () -> grammar_delete e pos rls),
                   (fun () -> G.extend e pos rls)))
       :: !camlp4_state;
       G.extend e pos rls
@@ -134,8 +143,8 @@ let rec remove_grammars n =
   if n>0 then
     (match !camlp4_state with
        | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
-       | ByGrammar(g,_,rls)::t ->
-           grammar_delete g rls;
+       | ByGrammar(g,pos,rls)::t ->
+           grammar_delete g pos rls;
            camlp4_state := t;
            remove_grammars (n-1)
        | ByGEXTEND (undo,redo)::t ->
@@ -487,7 +496,7 @@ let default_levels =
    90,Gramext.RightA;
    10,Gramext.RightA;
    9,Gramext.RightA;
-   5,Gramext.LeftA;
+   8,Gramext.LeftA;
    1,Gramext.LeftA;
    0,Gramext.RightA]