diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 869e65ca40..ff296c2dd3 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -260,6 +260,9 @@ val isCast : constr -> bool [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : constr -> constr +(* Special function, which keep the key casts under Fix and MutCase. *) +val strip_all_casts : constr -> constr + (* Destructs the product $(x:t_1)t_2$ *) val destProd : constr -> name * constr * constr val hd_of_prod : constr -> constr |