diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 28ebc41e24..50cd433e95 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -112,6 +112,7 @@ val isConstruct : constr -> bool val isFix : constr -> bool val isCoFix : constr -> bool val isCase : constr -> bool +val isProj : constr -> bool val is_Prop : constr -> bool val is_Set : constr -> bool @@ -183,6 +184,9 @@ return P in t1], or [if c then t1 else t2]) where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array +(** Destructs a projection *) +val destProj : constr -> projection * constr + (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} with f{_ 2} ctx{_ 2} = b{_ 2} |