diff options
| -rw-r--r-- | pretyping/reductionops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1df2a73b2e..51df07f286 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -90,6 +90,9 @@ module Stack : sig val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option val not_purely_applicative : 'a t -> bool + + (** @return the arguments in the stack if a purely applicative + stack, None otherwise *) val list_of_app_stack : constr t -> constr list option val assign : 'a t -> int -> 'a -> 'a t |