From 693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 25 Jun 2008 18:19:21 +0000
Subject: Création du fichier dumpglob.ml, qui rassemble les fonctions de
 globalisation (add_glob* et dump_*)

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

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index 08f9a279d1..4cab303815 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -61,9 +61,6 @@ val is_unsafe : string -> bool
 
 val noglob : bool ref
 val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-val dump_it : unit -> unit
 
 (* Options for the virtual machine *)
 
-- 
cgit v1.2.3