From 05c9f1ef3f608f1b2e92ef5a2556544ddb450b28 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Jan 2005 13:02:44 +0000
Subject: Code redondant (cf Printer)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6586 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/options.ml  | 2 --
 lib/options.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'lib')

diff --git a/lib/options.ml b/lib/options.ml
index ec9f0cb13d..f190519f1f 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -23,8 +23,6 @@ let debug = ref false
 
 let print_emacs = ref false
 
-let emacs_str s = if !print_emacs then s else "" 
-
 let term_quality = ref false
 
 let xml_export = ref false
diff --git a/lib/options.mli b/lib/options.mli
index bf935c76d3..1c07799509 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -17,7 +17,6 @@ val batch_mode : bool ref
 val debug : bool ref
 
 val print_emacs : bool ref
-val emacs_str : string -> string
 
 val term_quality : bool ref
 
-- 
cgit v1.2.3