diff options
| author | herbelin | 2002-12-10 09:38:39 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-10 09:38:39 +0000 |
| commit | 4affad97b01e15ccfb96a3a6a8c24964dbb4320d (patch) | |
| tree | 96c925dc17755278ff596b8a32d779f9a5799752 /toplevel | |
| parent | b094efba69a0289db5b431ef939bab124936b06d (diff) | |
Ajout options -v7 et -v8, et commandes V7only et V8only
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
3 files changed, 14 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c9fa6a18c2..a23ba7335c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -197,6 +197,10 @@ let parse_args () = | "-xml" :: rem -> Options.xml_export := true; parse rem + | "-v7" :: rem -> Options.v7 := true; parse rem + + | "-v8" :: rem -> Options.v7 := false; parse rem + | s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage () in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 4ad2c479ac..5dba3cdec8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -112,6 +112,12 @@ let rec vernac interpfun input = msgnl (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) + (* To be interpreted in v7 or translator input only *) + | VernacV7only v -> if !Options.v7 then interp v + + (* To be interpreted in translator output only *) + | VernacV8only v -> if true (* !translate *) then interp v + | v -> if not !just_parsing then interpfun v in diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index a11eadc7ec..adc46d2d19 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -260,6 +260,10 @@ type vernac_expr = (* Toplevel control *) | VernacToplevelControl of exn + (* For translation from V7 to V8 syntax *) + | VernacV8only of vernac_expr + | VernacV7only of vernac_expr + (* For extension *) | VernacExtend of string * raw_generic_argument list |