Moving unused code out of the kernel into Termops.

Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.

1 files changed, 0 insertions, 14 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 60a3c7715..a8d9dfbff 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr
 val strip_prod_assum : types -> types
 val strip_lam_assum : constr -> constr
 
-(** Flattens application lists *)
-val collapse_appl : constr -> constr
-
-
-(** Remove recursively the casts around a term i.e.
-   [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : constr -> constr
-
-(** Apply a function letting Casted types in place *)
-val under_casts : (constr -> constr) -> constr -> constr
-
-(** Apply a function under components of Cast if any *)
-val under_outer_cast : (constr -> constr) -> constr -> constr
-
 (** {5 ... } *)
 (** 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