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.

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

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 34538f21fd..93c12c3351 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1235,8 +1235,8 @@ let _ =
       optdepr  = false;
       optname  = "printing of existential variable instances";
       optkey   = ["Printing";"Existential";"Instances"];
-      optread  = (fun () -> !Constrextern.print_evar_arguments);
-      optwrite = (:=) Constrextern.print_evar_arguments }
+      optread  = (fun () -> !Detyping.print_evar_arguments);
+      optwrite = (:=) Detyping.print_evar_arguments }
 
 let _ =
   declare_bool_option
-- 
cgit v1.2.3