aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7e12d263a..a277864c9 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -100,7 +100,7 @@ module Stack : sig
@return the result and the lifts to apply on the terms
@raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
- constr t -> constr t -> 'a * int * int
+ constr t -> constr t -> 'a
val map : ('a -> 'a) -> 'a t -> 'a t
val append_app_list : 'a list -> 'a t -> 'a t