aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorherbelin2000-09-10 21:22:57 +0000
committerherbelin2000-09-10 21:22:57 +0000
commitc039e4e618d7da96909d42995eb21074945a3624 (patch)
treea58d5f6393afb1e66b1ee9e73f8bd492acc534be /parsing
parente72024e2292a50684b7f280d6efb8fee090e2dbf (diff)
Correction pour make doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/astterm.ml2
-rw-r--r--parsing/g_minicoq.ml42
-rw-r--r--parsing/pattern.ml2
-rw-r--r--parsing/pretty.ml2
-rw-r--r--parsing/termast.ml2
5 files changed, 5 insertions, 5 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 72b7e1cf55..1a2cc53aef 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -5,7 +5,7 @@ open Pp
open Util
open Names
open Sign
-(*i open Generic i*)
+(* open Generic *)
open Term
open Environ
open Evd
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index f3aaa4e2a7..ed8e9a5bff 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -5,7 +5,7 @@ open Pp
open Util
open Names
open Univ
-(*i open Generic i*)
+(* open Generic *)
open Term
open Environ
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 17a4535a4d..f84a2d929c 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -2,7 +2,7 @@
(* $Id$ *)
open Util
-(*i open Generic i*)
+(* open Generic *)
open Names
open Term
open Reduction
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 123f690a8b..d9e22af376 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -4,7 +4,7 @@
open Pp
open Util
open Names
-(*i open Generic i*)
+(* open Generic *)
open Term
open Declarations
open Inductive
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0d04bd2b21..b8a39e37fa 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -5,7 +5,7 @@ open Pp
open Util
open Univ
open Names
-(*i open Generic i*)
+(* open Generic *)
open Term
open Inductive
open Sign