aboutsummaryrefslogtreecommitdiffhomepage
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 2c84bd84d..2926e30e5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -31,7 +31,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : Vernacexpr.universe_decl_expr option;
- fix_annot : Id.t Loc.located option;
+ fix_annot : Misctypes.lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr