From a8f63f0dd852bf4510111feaf8bcdb7b4869c64d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 23 Aug 2014 01:11:40 +0200
Subject: Fixing bug #3533.

Now error printing tries to set universe printing when two terms are not
desambiguated.
---
 toplevel/himsg.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e3a303aed0..070c85eca3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -96,7 +96,10 @@ let explicit_flags =
   let open Constrextern in
   [ []; (** First, try with the current flags *)
     [print_implicits]; (** Then with implicit *)
-    [print_implicits; print_coercions; print_no_symbol] (** Then more! *) ]
+    [print_universes]; (** Then with universes *)
+    [print_universes; print_implicits]; (** With universes AND implicits *)
+    [print_implicits; print_coercions; print_no_symbol]; (** Then more! *)
+    [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]
 
 let pr_explicit env t1 t2 = pr_explicit_aux env t1 t2 explicit_flags
 
-- 
cgit v1.2.3