From d6405bd4b54465d2f1c259a6a0ea4bfe934e5a0c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 08:30:18 +0000
Subject: Options d'affichage maintenant dans Constrextern Ajout "Set/Unset
 Printing Implicits"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3846 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cb1f21149f..81bcd47352 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -760,8 +760,16 @@ let _ =
     { optsync  = true;
       optname  = "coercion printing";
       optkey   = (SecondaryTable ("Printing","Coercions"));
-      optread  = (fun () -> !Termast.print_coercions);
-      optwrite = (fun b ->  Termast.print_coercions := b) }
+      optread  = (fun () -> !Constrextern.print_coercions);
+      optwrite = (fun b ->  Constrextern.print_coercions := b) }
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "implicits printing";
+      optkey   = (SecondaryTable ("Printing","Implicits"));
+      optread  = (fun () -> !Constrextern.print_implicits);
+      optwrite = (fun b ->  Constrextern.print_implicits := b) }
 
 let _ =
   declare_bool_option 
-- 
cgit v1.2.3