diff options
Diffstat (limited to 'kernel/term.ml')
-rw-r--r-- | kernel/term.ml | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 33ed25fe1..7d47c4609 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -616,25 +616,6 @@ let decompose_lam_n_decls n = in lamdec_rec empty_rel_context n -(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction - * gives n (casts are ignored) *) -let nb_lam = - let rec nbrec n c = match kind_of_term c with - | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - -(* similar to nb_lam, but gives the number of products instead *) -let nb_prod = - let rec nbrec n c = match kind_of_term c with - | Prod (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - let prod_assum t = fst (decompose_prod_assum t) let prod_n_assum n t = fst (decompose_prod_n_assum n t) let strip_prod_assum t = snd (decompose_prod_assum t) |