aboutsummaryrefslogtreecommitdiff
path: root/kernel/closure.mli
diff options
context:
space:
mode:
authorfilliatr1999-08-19 08:17:17 +0000
committerfilliatr1999-08-19 08:17:17 +0000
commit10f4e87cca4f83700c9b6a8acffc081de66dc164 (patch)
tree71d963bff3495ecd124abc9466890f83d42577f0 /kernel/closure.mli
parent2178b546a941803548bd2699a860086ad8f5f1d5 (diff)
mise en place programmation literaire (generation de doc/coq.tex)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.mli')
-rw-r--r--kernel/closure.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 52f2ad038c..fb7431e4e7 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -1,12 +1,14 @@
(* $Id$ *)
+(*i*)
open Pp
open Names
open Generic
open Term
open Evd
open Environ
+(*i*)
(* flags for profiling... *)
val stats : bool ref