diff options
| author | Maxime Dénès | 2018-06-01 13:49:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-01 13:49:34 +0200 |
| commit | 3a36761a27487e8917e1b59b59abacc2a7e65b95 (patch) | |
| tree | f1cd9d412c40933ff3e87f720dbd8e7cba7f9bbf /interp/implicit_quantifiers.ml | |
| parent | ac0bb15616550d00f5e6e7d6239e3b7ff2632975 (diff) | |
| parent | 63b530234e0b19323a50c52434a7439518565c81 (diff) | |
Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 289890544f..b48db9ac54 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -17,12 +17,14 @@ open Glob_term open Constrexpr open Libnames open Typeclasses -open Typeclasses_errors open Pp open Libobject open Nameops open Context.Rel.Declaration +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) + module RelDecl = Context.Rel.Declaration (*i*) @@ -238,7 +240,7 @@ let implicit_application env ?(allow_partial=true) f ty = let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in if not (Int.equal needlen applen) then - Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in |