diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-25 16:48:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 00:11:44 +0200 |
| commit | 285bd0778bfa829e1969598cccd5d7c504d5fa90 (patch) | |
| tree | b497214820e5fbabf8a1445717fbc9ced3dccc3e /lib | |
| parent | c97a4b7bb4af07c22137e0933d041d1f7eea95f1 (diff) | |
Always print explanation for univ inconsistency, rm Flags.univ_print
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 3 |
2 files changed, 0 insertions, 4 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 8491873e0..2a1c50f52 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,7 +60,6 @@ let profile = false let ide_slave = ref false let raw_print = ref false -let univ_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 85aaf879f..53a69f356 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -42,9 +42,6 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -(* Univ print flag, never set anywere. Maybe should belong to Univ? *) -val univ_print : bool ref - type compat_version = V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int |