From 19a2dd5cfbd72defe932656a65ab9da9f4ac9d1e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 31 Oct 2016 20:25:28 +0100
Subject: 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.
---
 kernel/term.mli | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 60a3c77154..a8d9dfbfff 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
-- 
cgit v1.2.3