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. --- checker/term.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'checker/term.mli') diff --git a/checker/term.mli b/checker/term.mli index 0af83e05d..6b026d056 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -4,8 +4,6 @@ open Cic val family_of_sort : sorts -> sorts_family val family_equal : sorts_family -> sorts_family -> bool -val strip_outer_cast : constr -> constr -val collapse_appl : constr -> constr val decompose_app : constr -> constr * constr list val applist : constr * constr list -> constr val iter_constr_with_binders : -- cgit v1.2.3