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 b181984e0..36c2993af 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -32,7 +32,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
- fix_univs : Vernacexpr.universe_decl_expr option;
+ fix_univs : Constrexpr.universe_decl_expr option;
fix_annot : Misctypes.lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;