aboutsummaryrefslogtreecommitdiff
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 e60def72f6..59bc4a8b72 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -58,7 +58,7 @@ module Stack : sig
val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
type 'a case_stk =
- case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
+ case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array
type 'a member =
| App of 'a app_node