Correction sur commit précédent

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

4 files changed, 41 insertions, 21 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 6e8cfb05bf..c4e85dcecb 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -52,14 +52,17 @@ let find_position assoc = function
       let after = ref 8 in
       let rec add_level q = function
         | (p,_ as pa)::l when p > n -> pa :: add_level p l
-        | (p,a)::l when p = n -> raise (Found a)
-        | l -> after := q; (n,assoc)::l
+        | (p,a)::l when p = n ->
+	    if a = assoc or assoc = None then raise (Found a);
+	    after := q; (n,assoc)::l
+        | l ->
+	    after := q; (n,assoc)::l
       in
       try
         numeric_levels := add_level 8 !numeric_levels;
         Some (Gramext.After (constr_level !after)), assoc
       with
-          Found a -> Some (Gramext.Level (constr_level n)), a
+          Found _ -> Some (Gramext.Level (constr_level n)), assoc
 
 (* Interpretation of the right hand side of grammar rules *)
 
@@ -266,15 +269,14 @@ let rec interp_entry_name u s =
     let t, g = interp_entry_name u (String.sub s 0 (l-4)) in
     OptArgType t, Gramext.Sopt g
   else
-    let n = Extend.rename_command s in
-    let e = get_entry (get_univ u) n in
+    let e = get_entry (get_univ u) s in
     let o = object_of_typed_entry e in
     let t = type_of_typed_entry e in
     t,Gramext.Snterm (Pcoq.Gram.Entry.obj o)
 
 let qualified_nterm current_univ = function
-  | NtQual (univ, en) -> (rename_command univ, rename_command en)
-  | NtShort en -> (current_univ, rename_command en)
+  | NtQual (univ, en) -> (univ, en)
+  | NtShort en -> (current_univ, en)
 
 let make_vprod_item univ = function
   | VTerm s -> (Gramext.Stoken (Extend.terminal s), None)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index a689a59338..a53f0a31a2 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -147,7 +147,7 @@ let warn nt nt' =
   warning ("'"^nt^"' grammar entry is obsolete; use name '"^nt'^"' instead");
   nt'
 
-let rename_command nt =
+let rename_command_entry nt =
   if String.length nt >= 7 & String.sub nt 0 7 = "command"
   then warn nt ("constr"^(String.sub nt 7 (String.length nt - 7)))
   else if nt = "lcommand" then warn nt "lconstr"
@@ -178,18 +178,36 @@ let explicitize_prod_entry pos univ nt =
 
 let explicitize_entry = explicitize_prod_entry ()
 
-let qualified_nterm current_univ pos = function
+(* Express border sub entries in function of the from level and an assoc *)
+(* We're cheating: not necessarily the same assoc on right and left *)
+let clever_explicitize_prod_entry pos univ from en =
+  let t = explicitize_prod_entry pos univ en in
+  match explicitize_entry univ from with
+    | ETConstr (from,()) ->
+	(match t with
+	  | ETConstr (n,BorderProd (left,None)) when (n=from & left) ->
+	      ETConstr (n,BorderProd (true,Some Gramext.LeftA))
+	  | ETConstr (n,BorderProd (left,None)) when (n=from-1 & not left) ->
+	      ETConstr (n+1,BorderProd (true,Some Gramext.LeftA))
+	  | ETConstr (n,BorderProd (left,None)) when (n=from-1 & left) ->
+	      ETConstr (n+1,BorderProd (true,Some Gramext.RightA))
+	  | ETConstr (n,BorderProd (left,None)) when (n=from & not left) ->
+	      ETConstr (n,BorderProd (true,Some Gramext.RightA))
+	  | t -> t)
+    | _ -> t
+
+let qualified_nterm current_univ pos from = function
   | NtQual (univ, en) ->
-      explicitize_prod_entry pos (rename_command univ) (rename_command en)
+      clever_explicitize_prod_entry pos univ from en
   | NtShort en ->
-      explicitize_prod_entry pos current_univ (rename_command en)
+      clever_explicitize_prod_entry pos current_univ from en
 
 let check_entry check_entry_type = function
   | ETOther (u,n) -> check_entry_type (u,n)
   | _ -> ()
 
-let nterm loc ((check_entry_type,univ),pos) nont =
-  let typ = qualified_nterm univ pos nont in
+let nterm loc (((check_entry_type,univ),from),pos) nont =
+  let typ = qualified_nterm univ pos from nont in
   check_entry check_entry_type typ;
   typ
 
@@ -217,13 +235,11 @@ let gram_rule univ (name,pil,act) =
   { gr_name = name; gr_production = pilc; gr_action = a }
 
 let gram_entry univ (nt, ass, rl) =
-  let name = rename_command nt in
-  { ge_name = name;
+  { ge_name = nt;
     gl_assoc = ass;
-    gl_rules = List.map (gram_rule univ) rl }
+    gl_rules = List.map (gram_rule (univ,nt)) rl }
 
 let interp_grammar_command univ ge entryl =
-  let univ = rename_command univ in
   { gc_univ = univ;
     gc_entries = List.map (gram_entry (ge,univ)) entryl }
 
diff --git a/parsing/extend.mli b/parsing/extend.mli
index e55a417972..705fc88185 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -84,7 +84,7 @@ type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
 val terminal : string -> string * string
 
-val rename_command : string -> string
+val rename_command_entry : string -> string
 
 val explicitize_entry : string -> string -> constr_entry
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 4d675a0828..562a66e33e 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -214,7 +214,8 @@ GEXTEND Gram
 	  VernacTacticGrammar tl
 
      | "Grammar"; u = univ;
-         tl = LIST1 grammar_entry SEP "with" -> VernacGrammar (u,tl)
+         tl = LIST1 grammar_entry SEP "with" -> 
+	   VernacGrammar (rename_command_entry u,tl)
 
      | "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
@@ -294,8 +295,9 @@ GEXTEND Gram
            | _ -> VNonTerm (loc,nt,None) ]]
   ;
   non_terminal:
-    [[ u = IDENT; ":"; nt = IDENT -> NtQual(u, nt)
-     | nt = IDENT -> NtShort nt ]]
+    [[ u = IDENT; ":"; nt = IDENT ->
+        NtQual(rename_command_entry u, rename_command_entry nt)
+     | nt = IDENT -> NtShort (rename_command_entry nt) ]]
   ;