diff options
| author | herbelin | 2002-12-10 10:42:49 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-10 10:42:49 +0000 |
| commit | b230388e6843aea7dae6a662eee4bbe8acf8a79a (patch) | |
| tree | fa690a0015f13656c2bc96d03208cc878a6a7e1a /contrib/interface | |
| parent | cad1bcf2b780f362efac9b311ac3de9921f2689d (diff) | |
Ajout options -v7 et -v8, et commandes V7only et V8only
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3418 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 8 |
1 files changed, 6 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";; |