From 9fc63bfa8c8e8bc3bf835ebb2d3d444c5a6d4f9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 4 Dec 2014 10:47:31 +0100
Subject: Reactivating option "Set Printing Existential Instances" for asking
 printing full instances.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index c12f8a2760..49335a8039 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -24,8 +24,8 @@ open Genarg
 open Clenv
 open Universes
 
-let _ = Constrextern.print_evar_arguments := true
-let _ = Constrextern.print_universes := true
+let _ = Detyping.print_evar_arguments := true
+let _ = Detyping.print_universes := true
 let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
-- 
cgit v1.2.3