aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7af0a357ab..1f05e90bde 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -29,6 +29,7 @@ open Mod_subst
open Clenv
let _ = Constrextern.print_evar_arguments := true
+let _ = Constrextern.print_universes := true
let _ = set_bool_option_value ["Printing";"Matching"] false
let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)