From fa2571f711bf6ba6b99a04bf2cc10b68b37682f9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Apr 2003 10:28:25 +0000
Subject: Prise en compte affichage coercions traducteur dans Constrextern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3873 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/coqtop.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 130271aef6..99c1bed6f6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -169,7 +169,6 @@ let parse_args is_ide =
     | "-ftranslate" :: rem ->
         make_translate true;
         translate_file := true;
-        Constrextern.print_coercions := true;
         parse rem
 
     | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
-- 
cgit v1.2.3