From 285bd0778bfa829e1969598cccd5d7c504d5fa90 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 25 Apr 2018 16:48:10 +0200
Subject: 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)
---
 lib/flags.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e07..2a1c50f52b 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
 
-- 
cgit v1.2.3