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 | |
| 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
| -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 |