aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/implicit_quantifiers.ml')
-rw-r--r--interp/implicit_quantifiers.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 83ad9af33..288a0bfe0 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -22,7 +22,7 @@ open Libobject
open Nameops
open Context.Rel.Declaration
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
module RelDecl = Context.Rel.Declaration