diff options
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 ff53fca99a..f4f26994f9 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 ef75cde65d..51406b1e08 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 |