aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/ocaml.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-12-05 14:43:14 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-12-05 14:43:14 +0000
commitb86f8d977d9a0dd9635207e436bc1e59ca98475c (patch)
tree5c630a49ea16802fe3f60c1686e8080694a90338 /contrib/extraction/ocaml.mli
parentf4af459e05814c954514f71dcc4c63b00af823b5 (diff)
code cleanup (+ debut de commencement de modules)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.mli')
-rw-r--r--contrib/extraction/ocaml.mli4
1 files changed, 1 insertions, 3 deletions
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 41b370a50..da2706f68 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -11,11 +11,9 @@
(*s Some utility functions to be reused in module [Haskell]. *)
open Pp
-open Miniml
open Names
-open Term
open Libnames
-open Nametab
+open Miniml
val cons_cofix : Refset.t ref