aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/implicit_quantifiers.ml')
-rw-r--r--interp/implicit_quantifiers.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e8d10488b2..32290f0430 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -23,9 +23,6 @@ open Libobject
open Nameops
open Context.Rel.Declaration
-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
(*i*)