aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 16:06:42 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 16:06:42 +0000
commitccba6c718af6a5a15f278fc9365b6ad27108e98f (patch)
treef0229aa4d08eb12db1fb1e76f227076c117d59bf /kernel/term.mli
parent06456c76b7fa2f0c69380faf27a6ca403b1e6f3f (diff)
Various minor improvements of comments in mli for ocamldoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index 3940d74c5..f7819d6e6 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -64,7 +64,7 @@ val eq_constr : constr -> constr -> bool
type types = constr
-(** {6 Sect } *)
+(** {6 ... } *)
(** Functions for dealing with constr terms.
The following functions are intended to simplify and to uniform the
manipulation of terms. Some of these functions may be overlapped with
@@ -253,7 +253,7 @@ val is_Type : constr -> bool
val iskind : constr -> bool
val is_small : sorts -> bool
-(** {6 Sect } *)
+(** {6 ... } *)
(** Term destructors.
Destructor operations are partial functions and
raise [invalid_arg "dest*"] if the term has not the expected form. *)
@@ -319,7 +319,7 @@ val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
-(** {6 Sect } *)
+(** {6 ... } *)
(** A {e declaration} has the form (name,body,type). It is either an
{e assumption} if [body=None] or a {e definition} if
[body=Some actualbody]. It is referred by {e name} if [na] is an
@@ -483,7 +483,7 @@ val under_casts : (constr -> constr) -> constr -> constr
(** Apply a function under components of Cast if any *)
val under_outer_cast : (constr -> constr) -> constr -> constr
-(** {6 Sect } *)
+(** {6 ... } *)
(** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
Such a term can canonically be seen as the pair of a context of types
and of a sort *)