diff options
| -rw-r--r-- | lib/options.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 | ||||
| -rw-r--r-- | scripts/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
6 files changed, 26 insertions, 2 deletions
diff --git a/lib/options.ml b/lib/options.ml index a47a0bea8..cd0de97a4 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -24,6 +24,8 @@ let term_quality = ref false let xml_export = ref false +let v7 = ref true + (* Silent / Verbose *) let silent = ref false let make_silent flag = silent := flag; () diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 30c0d368b..57d799a15 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -41,8 +41,16 @@ GEXTEND Gram | c = syntax; "." -> c | n = natural; ":"; v = goal_vernac; "." -> v n | "["; l = vernac_list_tail -> VernacList l + + (* For translation from V7 to V8 *) + | IDENT "V7only"; v = vernac -> VernacV7only v + | IDENT "V8only"; v = vernac -> VernacV8only v + +(* (* This is for "Grammar vernac" rules *) - | id = METAIDENT -> VernacVar (Names.id_of_string id) ] ] + | id = METAIDENT -> VernacVar (Names.id_of_string id) +*) + ] ] ; goal_vernac: [ [ tac = Tactic.tactic -> fun n -> VernacSolve (n,tac) diff --git a/scripts/coqc.ml b/scripts/coqc.ml index fc1e57d78..4234216fa 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -136,7 +136,7 @@ let parse_args () = | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m"|"-xml" as o) :: rem -> + |"-silent"|"-m"|"-xml"|"-v7"|"-v8" as o) :: rem -> parse (cfiles,o::args) rem | ("-v"|"--version") :: _ -> Usage.version () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c9fa6a18c..a23ba7335 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 4ad2c479a..5dba3cdec 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 a11eadc7e..adc46d2d1 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 |