diff options
| author | Hugo Herbelin | 2015-11-08 09:54:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 08:58:20 +0100 |
| commit | 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 (patch) | |
| tree | fc399b19682aa528a73d90729c1e37ce4a761d6e /kernel/term.mli | |
| parent | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (diff) | |
Moving three related small half-general half-ad-hoc utility functions
next to each other, waiting for possible integration into a more
uniform API.
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 2bb8110608..69adb517a0 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -308,13 +308,6 @@ val decompose_lam_n_assum : int -> constr -> rel_context * constr (** Idem, counting let-ins *) val decompose_lam_n_decls : int -> constr -> rel_context * constr -(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction - gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : constr -> int - -(** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int - (** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context |