aboutsummaryrefslogtreecommitdiff
path: root/vernac/comFixpoint.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comFixpoint.mli')
-rw-r--r--vernac/comFixpoint.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a31f3c34e0..1ded9f3d29 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -57,7 +57,7 @@ val interp_recursive :
(* names / defs / types *)
(Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
(* ctx per mutual def / implicits / struct annotations *)
- (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
+ (EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Exported for Funind *)