diff options
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 1062d0e61b..445fcb7bc8 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -64,7 +64,10 @@ module type RedFlagsSig = sig (** Tests if a reduction kind is set *) val red_set : reds -> red_kind -> bool - + + (** This tests if the projection is in unfolded state already or + is unfodable due to delta. *) + val red_projection : reds -> projection -> bool end module RedFlags : RedFlagsSig @@ -113,7 +116,7 @@ type fterm = | FInd of inductive puniverses | FConstruct of constructor puniverses | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array |