diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-05 13:29:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-05 13:29:47 +0000 |
| commit | 49ae36f12977600e98435af7be73e0d961dfc2fb (patch) | |
| tree | ad4967f22d6609b39d8e7e44541c55503c6bdbd4 /kernel | |
| parent | 47bf3b7fee031096013b29ad496949de063f010a (diff) | |
doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/sign.mli | 9 | ||||
| -rw-r--r-- | kernel/term.mli | 3 |
2 files changed, 12 insertions, 0 deletions
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 |