diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
| commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
| tree | 9b221c283c2971f7ac151397231059e1d239e723 /kernel/term.mli | |
| parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
| parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) | |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |