aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.mli')
-rw-r--r--vernac/classes.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli
index bd30b2d60..9c37364cb 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -16,9 +16,9 @@ open Libnames
(** Errors *)
-val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
+val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a
-val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
+val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
(** Instance declaration *)