Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'

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

2 files changed, 8 insertions, 4 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index ff3d827d9..26c76e594 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -106,7 +106,7 @@ let execute_when_necessary ast =
 let execute_when_necessary v =
  (match v with
   | VernacGrammar _ -> Vernacentries.interp v
-  | VernacOpenScope sc -> Vernacentries.interp v
+  | VernacOpenCloseScope sc -> Vernacentries.interp v
   | VernacRequire (_,_,l) ->
       (try 
 	Vernacentries.interp v
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3ebad5ae3..b7fbd7fc8 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1475,7 +1475,8 @@ let xlate_vernac =
         | PrintModuleType _ -> xlate_error "TODO: Print Module Type"
         | PrintModule _ -> xlate_error "TODO: Print Module"
         | PrintScopes -> xlate_error "TODO: Print Scopes"
-        | PrintScope _ -> xlate_error "TODO: Print Scope")
+        | PrintScope _ -> xlate_error "TODO: Print Scope"
+        | PrintAbout _ -> xlate_error "TODO: Print About")
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment id -> CT_section_end (xlate_ident id)
@@ -1616,7 +1617,7 @@ let xlate_vernac =
          	| ("SYNTAX", [Varg_ident phy; Varg_ident s; spatarg; unparg]) ->
          	        (syntaxop phy s spatarg unparg 
          coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*)
-   | VernacOpenScope sc -> xlate_error "TODO: open scope"
+   | VernacOpenCloseScope sc -> xlate_error "TODO: open/close scope"
 
    | VernacArgumentsScope _ -> xlate_error "TODO: Arguments Scope"
 
@@ -1628,7 +1629,9 @@ let xlate_vernac =
 
    | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
 
-   | VernacInfix (false,str_assoc, Some n, str, id, false, _, None) ->
+   | VernacInfix (false,(str,modl),id,_,None) ->
+       (match Metasyntax.interp_infix_modifiers modl with
+	 | (str_assoc,Some n,false,None) ->
       CT_infix (
        (match str_assoc with
         | Some Gramext.LeftA -> CT_lefta
@@ -1636,6 +1639,7 @@ let xlate_vernac =
         | Some Gramext.NonA -> CT_nona
         | None -> CT_coerce_NONE_to_ASSOC CT_none),
        CT_int n, CT_string str, loc_qualid_to_ct_ID id)
+	 | _ -> xlate_error "TODO: handle onlyparse and format")
    | VernacInfix _ -> xlate_error "TODO: handle scopes and locality"
    | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
    | VernacCoercion (s, id1, id2, id3) ->