From 49ae36f12977600e98435af7be73e0d961dfc2fb Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 5 May 2000 13:29:47 +0000
Subject: doc

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

diff --git a/kernel/sign.mli b/kernel/sign.mli
index ff53fca99..f4f26994f 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -20,8 +20,17 @@ val map_sign_typ : ('a -> 'b) -> 'a signature -> 'b signature
 val isnull_sign : 'a signature -> bool
 val hd_sign : 'a signature -> identifier * 'a
 val tl_sign : 'a signature -> 'a signature
+
+(* [sign_it f sign a] iters [f] on [sign] starting from [a] and
+   peeling [sign] from the oldest declaration *)
+
 val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
+
+(* [it_sign f a sign] iters [f] on [sign] starting from [a] and
+   peeling [sign] from the more recent declaration *)
+
 val it_sign : ('b -> identifier -> 'a -> 'b) -> 'b -> 'a signature -> 'b
+
 val concat_sign : 'a signature -> 'a signature -> 'a signature
 
 val ids_of_sign : 'a signature -> identifier list
diff --git a/kernel/term.mli b/kernel/term.mli
index ef75cde65..51406b1e0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -356,6 +356,9 @@ val abs_implicit : constr -> constr
 val lambda_implicit : constr -> constr
 val lambda_implicit_lift : int -> constr -> constr
 
+(* [applist (f,args)] and co build [mkAppL (f,args)] if [args] non
+   empty and build [f] otherwise *)
+
 val applist : constr * constr list -> constr
 val applistc : constr -> constr list -> constr
 val appvect : constr * constr array -> constr
-- 
cgit v1.2.3