From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- kernel/term.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index d5899f18..e83be6d6 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -229,8 +229,9 @@ val kind_of_type : types -> (constr, types) kind_of_type (** {6 Simple term case analysis. } *) val isRel : constr -> bool +val isRelN : int -> constr -> bool val isVar : constr -> bool -val isVarId : identifier -> constr -> bool +val isVarId : identifier -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool @@ -435,8 +436,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types (** {6 Other term destructors. } *) (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair - {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. - It includes also local definitions *) + {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) val decompose_prod : constr -> (name*constr) list * constr (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair -- cgit v1.2.3