diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-23 01:11:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-23 01:12:11 +0200 |
| commit | a8f63f0dd852bf4510111feaf8bcdb7b4869c64d (patch) | |
| tree | aed95dd5d4b5bed8f8874d516a24e727c32e72c5 | |
| parent | 47fbb3a74b9bd52b19e63e695fb1902ed345488e (diff) | |
Fixing bug #3533.
Now error printing tries to set universe printing when two terms are not
desambiguated.
| -rw-r--r-- | toplevel/himsg.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e3a303aed..070c85eca 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 |