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)

7 files changed, 15 insertions, 17 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9b402586..8d5b5bef4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d1644614..b4ea04a56 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -21,7 +21,7 @@ open Univ
 (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu
    Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
 
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
   raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
 
 (* Universes are stratified by a partial ordering $\le$.
@@ -557,8 +557,7 @@ let get_explanation strict u v g =
   else match traverse strict u with Some exp -> exp | None -> assert false
 
 let get_explanation strict u v g =
-  if !Flags.univ_print then Some (get_explanation strict u v g)
-  else None
+  Some (lazy (get_explanation strict u v g))
 
 (* To compare two nodes, we simply do a forward search.
    We implement two improvements:
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ea3a52295..8e19fa4e5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -541,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
 
-type univ_inconsistency = constraint_type * universe * universe * explanation option
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
 
 exception UniverseInconsistency of univ_inconsistency
 
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
   raise (UniverseInconsistency (o,make u,make v,p))
 
 (* Constraints and sets of constraints. *)    
@@ -1235,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) =
     | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" 
   in
   let reason = match p with
-    | None | Some [] -> mt()
+    | None -> mt()
     | Some p ->
-      str " because" ++ spc() ++ pr_uni v ++
+      let p = Lazy.force p in
+      if p = [] then mt ()
+      else
+        str " because" ++ spc() ++ pr_uni v ++
 	prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
-	p ++
+          p ++
 	(if Universe.equal (snd (List.last p)) u then mt() else
-	    (spc() ++ str "= " ++ pr_uni u)) 
+           (spc() ++ str "= " ++ pr_uni u))
   in
     str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
       pr_rel o ++ spc() ++ pr_uni v ++ reason
diff --git a/kernel/univ.mli b/kernel/univ.mli
index aaed899bf..b68bbdf35 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -205,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function
   Constraint.t...
 *)
 type explanation = (constraint_type * Universe.t) list
-type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option
+type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
 
 exception UniverseInconsistency of univ_inconsistency
 
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
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb563220b..56e582891 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -36,7 +36,7 @@ type _ delay =
 | Later : [ `thunk ] delay
 
 (** Should we keep details of universes during detyping ? *)
-let print_universes = Flags.univ_print
+let print_universes = ref false
 
 (** If true, prints local context of evars, whatever print_arguments *)
 let print_evar_arguments = ref false