8 files changed, 39 insertions, 21 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f61dd0c101..019c0a6819 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -384,8 +384,26 @@ let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
 
+(* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
+let same_flags {
+     check_guarded;
+     check_universes;
+     conv_oracle;
+     share_reduction;
+     enable_VM;
+     enable_native_compiler;
+  } alt =
+  check_guarded == alt.check_guarded &&
+  check_universes == alt.check_universes &&
+  conv_oracle == alt.conv_oracle &&
+  share_reduction == alt.share_reduction &&
+  enable_VM == alt.enable_VM &&
+  enable_native_compiler == alt.enable_native_compiler
+[@warning "+9"]
+
 let set_typing_flags c env = (* Unsafe *)
-  { env with env_typing_flags = c }
+  if same_flags env.env_typing_flags c then env
+  else { env with env_typing_flags = c }
 
 (* Global constants *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index bab2eae3df..0dde1c7e75 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -47,10 +47,9 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.AUContext.t
+  | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 8e7e618fcd..0acd09fb12 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -106,10 +106,9 @@ type signature_mismatch_error =
   | RecordFieldExpected of bool
   | RecordProjectionsExpected of Name.t list
   | NotEqualInductiveAliases
-  | IncompatibleInstances
   | IncompatibleUniverses of Univ.univ_inconsistency
   | IncompatiblePolymorphism of env * types * types
-  | IncompatibleConstraints of Univ.AUContext.t
+  | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
 
 type module_typing_error =
   | SignatureMismatch of
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index df10398b2f..2464df799e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -192,7 +192,9 @@ let set_engagement c senv =
     engagement = Some c }
 
 let set_typing_flags c senv =
-  { senv with env = Environ.set_typing_flags c senv.env }
+  let env = Environ.set_typing_flags c senv.env in
+  if env == senv.env then senv
+  else { senv with env }
 
 let set_share_reduction b senv =
   let flags = Environ.typing_flags senv.env in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d64342dbb0..347c30dd64 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -93,10 +93,8 @@ let check_conv_error error why cst poly f env a1 a2 =
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
 let check_polymorphic_instance error env auctx1 auctx2 =
-  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
-    error IncompatibleInstances
-  else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
-    error (IncompatibleConstraints auctx1)
+  if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
   else
     Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9ff51fca55..9083156745 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -942,34 +942,36 @@ let check_eq_instances g t1 t2 =
 
 (** Pretty-printing *)
 
+let pr_umap sep pr map =
+  let cmp (u,_) (v,_) = Level.compare u v in
+  Pp.prlist_with_sep sep pr (List.sort cmp (UMap.bindings map))
+
 let pr_arc prl = function
   | _, Canonical {univ=u; ltle; _} ->
     if UMap.is_empty ltle then mt ()
     else
       prl u ++ str " " ++
       v 0
-        (pr_sequence (fun (v, strict) ->
+        (pr_umap Pp.spc (fun (v, strict) ->
           (if strict then str "< " else str "<= ") ++ prl v)
-           (UMap.bindings ltle)) ++
+           ltle) ++
       fnl ()
   | u, Equiv v ->
       prl u  ++ str " = " ++ prl v ++ fnl ()
 
 let pr_universes prl g =
-  let graph = UMap.fold (fun u a l -> (u,a)::l) g.entries [] in
-  prlist (pr_arc prl) graph
+  pr_umap mt (pr_arc prl) g.entries
 
 (* Dumping constraints to a file *)
 
 let dump_universes output g =
   let dump_arc u = function
     | Canonical {univ=u; ltle; _} ->
-        let u_str = Level.to_string u in
         UMap.iter (fun v strict ->
           let typ = if strict then Lt else Le in
-          output typ u_str (Level.to_string v)) ltle;
+          output typ u v) ltle;
     | Equiv v ->
-      output Eq (Level.to_string u) (Level.to_string v)
+      output Eq u v
   in
   UMap.iter dump_arc g.entries
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4336a22b8c..a2cc5b3116 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -86,7 +86,7 @@ val check_subtype : AUContext.t check_function
 (** {6 Dumping to a file } *)
 
 val dump_universes :
-  (constraint_type -> string -> string -> unit) -> t -> unit
+  (constraint_type -> Level.t -> Level.t -> unit) -> t -> unit
 
 (** {6 Debugging} *)
 val check_universes_invariants : t -> unit
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0edf750997..2b3b4f9486 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -570,9 +570,9 @@ struct
   include S
 
   let pr prl c =
-    fold (fun (u1,op,u2) pp_std ->
-      pp_std ++ prl u1 ++ pr_constraint_type op ++
-	prl u2 ++ fnl () )  c (str "")
+    v 0 (prlist_with_sep spc (fun (u1,op,u2) ->
+      hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2))
+       (elements c))
 
 end