diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d404a7e414..7a840c5731 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -73,6 +73,7 @@ module Stack : sig val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + [@@ocaml.deprecated "Use decomp_rev"] val compare_shape : 'a t -> 'a t -> bool @@ -93,6 +94,9 @@ module Stack : sig (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option + (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *) + val decomp_rev : 'a t -> ('a * 'a t) option + val not_purely_applicative : 'a t -> bool val list_of_app_stack : constr t -> constr list option |