diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
2 files changed, 7 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 91bd1a13be..c9079a8fc1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1521,7 +1521,8 @@ let xlate_vernac = (CT_ident s, CT_varg_list (List.map coerce_genarg_to_VARG l)) | VernacDebug b -> xlate_error "TODO: Debug On/Off" - | VernacList l -> xlate_error "Not treated here" + | (VernacList _ | VernacV7only _ | VernacV8only _) -> + xlate_error "Not treated here" | VernacNop -> CT_proof_no_op | VernacComments l -> CT_scomments(CT_scomment_content_list (List.map xlate_comment l)) @@ -1547,10 +1548,13 @@ let xlate_vernac = | VernacDeclareModule _ -> xlate_error "TODO: vernac" | VernacDeclareModuleType _ -> xlate_error "TODO: vernac" -let xlate_vernac_list = +let rec xlate_vernac_list = function | VernacList (v::l) -> CT_command_list (xlate_vernac (snd v), List.map (fun (_,x) -> xlate_vernac x) l) + | VernacV7only v -> + if !Options.v7 then xlate_vernac_list v + else xlate_error "Unknown command" | VernacList [] -> xlate_error "xlate_command_list" | _ -> xlate_error "Not a list of commands";; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d30968df64..7213727c22 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1029,6 +1029,7 @@ let _ = let interp c = match c with (* Control (done in vernac) *) | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false + | (VernacV7only _ | VernacV8only _) -> assert false (* Syntax *) | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel |