Utilisation de Snext pour gérer les symboles non associatifs

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

3 files changed, 18 insertions, 14 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 42a23b4c85..ade148afec 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -45,11 +45,6 @@ let constr_level = function
   | 8,assoc -> assert (assoc <> Gramext.LeftA); "top"
   | n,assoc -> (string_of_int n)^(assoc_level assoc)
 
-let constr_prod_level = function
-  | 8 -> "top"
-  | 4 -> "4L"
-  | n -> string_of_int n
-
 let default_levels = [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA]
 let level_stack = ref [default_levels]
 
@@ -191,11 +186,7 @@ let rec build_prod_item univ assoc = function
   | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc s)
   | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc s)
   | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc s)
-  | ProdPrimitive typ ->
-      match get_constr_production_entry assoc typ with
-	| (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj)
-	| (eobj,Some lev) -> 
-	    Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev)
+  | ProdPrimitive typ -> symbol_of_production assoc typ
 
 let symbol_of_prod_item univ assoc = function
   | Term tok -> (Gramext.Stoken tok, None)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 9a6caf41d7..fa67fe675a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -510,15 +510,16 @@ let coq_assoc = function
 
 let adjust_level assoc = function
   (* If no associativity constraints, adopt the current one *)
+  | (n,BorderProd (false,Some Gramext.NonA)) -> Some None
   | (n,BorderProd (_,Some Gramext.NonA)) -> None
   (* Otherwise, deal with the current one *)
   | (n,BorderProd (_,a)) when coq_assoc a = camlp4_assoc assoc -> None
   | (n,BorderProd (left,a)) ->
       let a = coq_assoc a in
       if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA)
-      then Some n else Some (n-1)
+      then Some (Some n) else Some (Some (n-1))
   | (8,InternalProd) -> None
-  | (n,InternalProd) -> Some n
+  | (n,InternalProd) -> Some (Some n)
 
 let compute_entry allow_create adjust = function
   | ETConstr (10,_) -> weaken_entry Constr.lconstr, None
@@ -537,3 +538,15 @@ let compute_entry allow_create adjust = function
 
 let get_constr_entry = compute_entry true (fun (n,()) -> Some n)
 let get_constr_production_entry ass = compute_entry false (adjust_level ass)
+
+let constr_prod_level = function
+  | 8 -> "top"
+  | 4 -> "4L"
+  | n -> string_of_int n
+
+let symbol_of_production assoc typ =
+  match get_constr_production_entry assoc typ with
+    | (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj)
+    | (eobj,Some None) -> Gramext.Snext
+    | (eobj,Some (Some lev)) -> 
+        Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c185c9309e..f643b408d6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -35,8 +35,8 @@ val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
 val get_constr_entry :
   constr_entry -> grammar_object Gram.Entry.e * int option
 
-val get_constr_production_entry : Gramext.g_assoc option -> 
-  constr_production_entry -> grammar_object Gram.Entry.e * int option
+val symbol_of_production : Gramext.g_assoc option -> 
+  constr_production_entry -> Token.t Gramext.g_symbol
 
 val grammar_extend :
   'a Gram.Entry.e -> Gramext.position option ->