diff options
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d9f15337..3106e866 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -128,9 +128,12 @@ type instance_flag = bool option (* Some true = Backward instance; Some false = type export_flag = bool (* true = Export; false = Import *) type specif_flag = bool (* true = Specification; false = Implementation *) type inductive_flag = Decl_kinds.recursivity_kind -type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) +type onlyparsing_flag = Flags.compat_version option + (* Some v = Parse only; None = Print also. + If v<>Current, it contains the name of the coq version + which this notation is trying to be compatible with *) type option_value = Goptionstyp.option_value = | BoolValue of bool @@ -189,7 +192,7 @@ type syntax_modifier = | SetLevel of int | SetAssoc of gram_assoc | SetEntryType of string * simple_constr_prod_entry_key - | SetOnlyParsing + | SetOnlyParsing of Flags.compat_version | SetFormat of string located type proof_end = @@ -377,13 +380,20 @@ let rec is_navigation_vernac = function | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true + | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *) | c -> is_deep_navigation_vernac c and is_deep_navigation_vernac = function - | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l | _ -> false +(* NB: Reset is now allowed again as asked by A. Chlipala *) + +let is_reset = function + | VernacResetInitial | VernacResetName _ -> true + | _ -> false + (* Locating errors raised just after the dot is parsed but before the interpretation phase *) |