aboutsummaryrefslogtreecommitdiff
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 3039269671..1982a08fd3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -161,7 +161,7 @@ and cofixpoint_expr =
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
- | CMeasureRec of constr_expr
+ | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
(** Anonymous defs allowed ?? *)
and local_binder =