diff options
| author | Théo Zimmermann | 2019-11-13 15:50:39 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-02 17:23:22 +0100 |
| commit | 88fe0bcf86ad6cb95ffacfcd37f51fa3ae2da4fc (patch) | |
| tree | 05a0ed1f5d31789ea0457fe6caf5df0c95050c5e /vernac/vernacexpr.ml | |
| parent | fcf5d724b5bd26581ecad6055ee33d2758133854 (diff) | |
Remove deprecated compat modifier of Notation / Infix commands.
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index bec6a0d2bb..32ff8b8fb2 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -105,7 +105,7 @@ 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 = Declarations.recursivity_kind -type onlyparsing_flag = Flags.compat_version option +type onlyparsing_flag = { onlyparsing : bool } (* 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 *) @@ -185,7 +185,6 @@ type syntax_modifier = | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing | SetOnlyPrinting - | SetCompatVersion of Flags.compat_version | SetFormat of string * lstring type proof_end = |