aboutsummaryrefslogtreecommitdiff
path: root/vernac/comFixpoint.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comFixpoint.mli')
-rw-r--r--vernac/comFixpoint.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index f4569ed3e2..338dfa5ef5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -78,6 +78,7 @@ val interp_fixpoint :
(EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Registering fixpoints and cofixpoints in the environment *)
+
(** [Not used so far] *)
val declare_fixpoint :
locality -> polymorphic ->