From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- kernel/term.ml | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 455248dd5..2060c7b6e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -486,8 +486,6 @@ let lambda_applist c l = let lambda_appvect c v = lambda_applist c (Array.to_list v) -let lambda_app c a = lambda_applist c [a] - let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then @@ -501,15 +499,6 @@ let lambda_applist_assum n c l = let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) -(* pseudo-reduction rule: - * [prod_app s (Prod(_,B)) N --> B[N] - * with an strip_outer_cast on the first argument to produce a product *) - -let prod_app t n = - match kind_of_term (strip_outer_cast t) with - | Prod (_,_,b) -> subst1 n b - | _ -> anomaly (str"Needed a product, but didn't find one") - (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist c l = let rec app subst c l = -- cgit v1.2.3