diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 568d8a38ec..37f25e0ac4 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -122,9 +122,12 @@ type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) 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 = Interface.option_value = | BoolValue of bool @@ -183,7 +186,7 @@ type syntax_modifier = | SetLevel of int | SetAssoc of Compat.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing + | SetOnlyParsing of Flags.compat_version | SetFormat of string located type proof_end = |