aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 073f9ba0b..4e2017f44 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -114,7 +114,7 @@ type constr_expr =
| CDynamic of loc * Dyn.t
and fixpoint_expr =
- identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
identifier * local_binder list * constr_expr * constr_expr