diff options
| author | Hugo Herbelin | 2015-07-03 21:28:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 19:13:52 +0200 |
| commit | 21e41af41b52914469885f40155702f325d5c786 (patch) | |
| tree | 5bc47400b40badbc2e9edf9687e3bbb69eed6ad3 | |
| parent | 7532f3243ba585f21a8f594d3dc788e38dfa2cb8 (diff) | |
Documenting in passing.
| -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 |