From e1d0e117652115b05faec1c276b9f14c5bf70d1f Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 4 Apr 2001 09:19:15 +0000
Subject: documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1530 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extraction.mli | 2 ++
 contrib/extraction/miniml.mli     | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 8ad3f7556e..100028f141 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -8,6 +8,8 @@
 
 (*i $Id$ i*)
 
+(*s Extraction from Coq terms to Miniml. *)
+
 open Names
 open Term
 open Miniml
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 1699486562..12702e38ce 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -8,12 +8,12 @@
 
 (*i $Id$ i*)
 
+(*s Target language for extraction: a core ML called MiniML. *)
+
 open Pp
 open Names
 open Term
 
-(*s Target language for extraction: a core ML called MiniML. *)
-
 (*s ML type expressions. *)
 
 type ml_type = 
-- 
cgit v1.2.3