From 6c3dc5c013654a7fe50d2ae23e834560e1637f15 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 2 Jun 2000 13:08:23 +0000
Subject: doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@492 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.mli | 4 ++--
 kernel/term.mli      | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 936c9093ae..33f85d800b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -20,12 +20,12 @@ corresponds to a [mutual_inductive_instance =
 mutual_inductive_body * constr list]. One inductive type in an
 instanciated packet corresponds to an [inductive_instance =
 mutual_inductive_instance * int]. Applying global parameters to an
-inductive_instance gives an [inductive_family = inductive_instance *
+[inductive_instance] gives an [inductive_family = inductive_instance *
 constr list]. Finally, applying real parameters gives an
 [inductive_type = inductive_family * constr list]. At each level
 corresponds various appropriated functions *)
 
-type inductive_instance (* ex-mind_specif *)
+type inductive_instance (* ex-[mind_specif] *)
 
 val mis_index : inductive_instance -> int
 val mis_ntypes : inductive_instance -> int
diff --git a/kernel/term.mli b/kernel/term.mli
index 787f51c63b..69bd7d644f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -548,7 +548,7 @@ val occur_evar : existential_key -> constr -> bool
    in c, [false] otherwise *)
 val occur_var : identifier -> 'a term -> bool
 
-(* [dependent M N] is true iff M is eq_constr with a subterm of N 
+(* [dependent M N] is true iff M is eq\_constr with a subterm of N 
    M is appropriately lifted through abstractions of N *)
 val dependent : constr -> constr -> bool
 
-- 
cgit v1.2.3