diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 51df07f286..1df2a73b2e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -90,9 +90,6 @@ 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 |