From 35ff578d093b3616af1280dd768e2afc96a8e09e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 16:34:37 +0200
Subject: Deduce Stack.decomp from Stack.strip_n_app.

---
 pretyping/reductionops.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'pretyping/reductionops.mli')

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
 
-- 
cgit v1.2.3


From 82fffac9b316f3ff31a5dd297e79f948b8749250 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Oct 2020 16:42:40 +0200
Subject: Documenting module Reductionops.Stack.

Also includes minor layout or code changes.
---
 pretyping/reductionops.mli | 33 ++++++++++++++++++++++++++++-----
 1 file changed, 28 insertions(+), 5 deletions(-)

(limited to 'pretyping/reductionops.mli')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7a840c5731..29b698f9d6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -69,8 +69,6 @@ module Stack : sig
 
   val empty : 'a t
   val is_empty : 'a t -> bool
-  val append_app : 'a array -> 'a t -> 'a t
-  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"]
@@ -85,26 +83,51 @@ module Stack : sig
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a
   val map : ('a -> 'a) -> 'a t -> 'a t
+
+  (** [append_app args sk] pushes array of arguments [args] on [sk] *)
+  val append_app : 'a array -> 'a t -> 'a t
+
+  (** [append_app_list args sk] pushes list of arguments [args] on [sk] *)
   val append_app_list : 'a list -> 'a t -> 'a t
 
-  (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
-      start by App *)
+  (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with
+      [sk1] purely applicative and [sk2] does not start with an argument *)
   val strip_app : 'a t -> 'a t * 'a t
 
-  (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
+  (** @return (the nth first elements, the (n+1)th element, the remaining stack)
+      if there enough of those *)
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
+  (** [decomp sk] extracts the first argument of [sk] is there is some *)
+  val decomp : '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
 
+  (** [not_purely_applicative sk] *)
   val not_purely_applicative : 'a t -> bool
+
+  (** [list_of_app_stack sk] either returns [Some sk] turned into a list of
+      arguments if [sk] is purely applicative and [None] otherwise *)
   val list_of_app_stack : constr t -> constr list option
 
+  (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0
+      @raise an anomaly if there is less that [n] arguments available *)
   val assign : 'a t -> int -> 'a -> 'a t
+
+  (** [args_size sk] returns the number of arguments available at the
+      head of [sk] *)
   val args_size : 'a t -> int
+
+  (** [tail n sk] drops the [n] first arguments of [sk]
+      @raise [Invalid_argument] if there are not enough arguments *)
   val tail : int -> 'a t -> 'a t
+
+  (** [nth sk n] returns the [n]-th argument of [sk], counting from 0
+      @raise [Not_found] if there is no [n]th argument *)
   val nth : 'a t -> int -> 'a
 
+  (** [zip sigma t sk] *)
   val zip : evar_map -> constr * constr t -> constr
 end
 
-- 
cgit v1.2.3