aboutsummaryrefslogtreecommitdiff
path: root/vernac/comFixpoint.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comFixpoint.mli')
-rw-r--r--vernac/comFixpoint.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a19b96f0f3..dcb61d38d9 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -58,7 +58,8 @@ val interp_recursive :
(** Exported for Funind *)
val interp_fixpoint
- : cofix:bool
+ : ?check_recursivity:bool ->
+ cofix:bool
-> lident option fix_expr_gen list
-> (Constr.t, Constr.types) recursive_preentry *
UState.universe_decl * UState.t *