diff options
| -rw-r--r-- | contrib/interface/parse.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 10 |
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) -> |