On n'autorise plus les niveaux doubles L/R en v8

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

1 files changed, 1 insertions, 86 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 6d1d317e6..4f583424e 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -37,90 +37,6 @@ let (grammar_state : all_grammar_command list ref) = ref []
 
 
 (**************************************************************************)
-let assoc_level = function
-  | Gramext.LeftA -> "L"
-  | _ -> ""
-
-let constr_level = function
-  | n,assoc -> (string_of_int n)^(assoc_level assoc)
-
-let default_levels_v7 =
-  [10,Gramext.RightA;
-   9,Gramext.RightA;
-   8,Gramext.RightA;
-   1,Gramext.RightA;
-   0,Gramext.RightA]
-
-let default_levels_v8 =
-  [200,Gramext.RightA;
-   100,Gramext.RightA;
-   80,Gramext.RightA;
-   10,Gramext.LeftA;
-   9,Gramext.RightA;
-   1,Gramext.LeftA;
-   0,Gramext.RightA]
-
-let level_stack = ref [default_levels_v7]
-
-(* At a same level, LeftA takes precedence over RightA and NoneA *)
-(* In case, several associativity exists for a level, we make two levels, *)
-(* first LeftA, then RightA and NoneA together *)
-exception Found of Gramext.g_assoc
-
-open Ppextend
-
-let admissible_assoc = function
-  | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
-  | Gramext.RightA, Some Gramext.LeftA -> false
-  | _ -> true
-
-let create_assoc = function
-  | None -> Gramext.RightA
-  | Some a -> a
-
-let find_position other assoc lev =
-  let default =
-    if !Options.v7 then (10,Gramext.RightA) else (200,Gramext.RightA) in
-  let current = List.hd !level_stack in 
-  match lev with
-  | None ->
-      level_stack := current :: !level_stack;
-      None, (if other then assoc else None), None
-  | Some n ->
-      if !Options.v7 & n = 8 & assoc = Some Gramext.LeftA then 
-	error "Left associativity not allowed at level 8";
-      let after = ref default in
-      let rec add_level q = function
-        | (p,_ as pa)::l when p > n -> pa :: add_level pa l
-        | (p,a as pa)::l as l' when p = n ->
-	    if admissible_assoc (a,assoc) then raise (Found a);
-	    (* Maybe this was (p,Right) and p occurs a second time *)
-	    if a = Gramext.LeftA then
-	      match l with
-		| (p,a)::_ as l' when p = n -> raise (Found a)
-		| _ -> after := pa; pa::(n,create_assoc assoc)::l
-	    else
-	      (* This was not (p,LeftA) hence assoc is RightA *)
-	      (after := q; (n,create_assoc assoc)::l')
-	| l ->
-	    after := q; (n,create_assoc assoc)::l
-      in
-      try
-	(* Create the entry *)
-        let current = List.hd !level_stack in
-        level_stack := add_level default current :: !level_stack;
-	let assoc = create_assoc assoc in
-        Some (Gramext.After (constr_level !after)),
-	Some assoc, Some (constr_level (n,assoc))
-      with
-          Found a ->
-            level_stack := current :: !level_stack;
-	    (* Just inherit the existing associativity and name (None) *)
-	    Some (Gramext.Level (constr_level (n,a))), None, None
-
-let remove_levels n =
-  level_stack := list_skipn n !level_stack
-
 (* Interpretation of the right hand side of grammar rules *)
 
 (* When reporting errors, we add the name of the grammar rule that failed *)
@@ -458,8 +374,7 @@ let reset_extend_grammars_v8 () =
   tac_exts := [];
   vernac_exts := [];
   List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
-  List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv;
-  level_stack := [default_levels_v8]
+  List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
 
 
 (* Summary functions: the state of the lexer is included in that of the parser.