Merge PR #10226: Simplify implicit_quantifiers

Reviewed-by: herbelin

5 files changed, 4 insertions, 32 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index bd5a211f1d..178387dd17 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -281,9 +281,6 @@ let existing_instance glob g info =
                          ~hdr:"declare_instance"
                          (Pp.str "Constant does not build instances of a declared type class.")
 
-let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m
-let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m
-
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
 let type_ctx_instance ~program_mode env sigma ctx inst subst =
@@ -479,9 +476,8 @@ let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx'
 let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props =
   let term, termtype, sigma =
     match props with
-    | (true, { CAst.v = CRecord fs }) ->
-      if List.length fs > List.length k.cl_props then
-        mismatched_props env' (List.map snd fs) k.cl_props;
+    | (true, { CAst.v = CRecord fs; loc }) ->
+      check_duplicate ?loc fs;
       let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in
       let term, termtype =
         do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
@@ -502,9 +498,8 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp
 let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
   let term, termtype, sigma =
     match opt_props with
-    | Some (true, { CAst.v = CRecord fs }) ->
-      if List.length fs > List.length k.cl_props then
-        mismatched_props env' (List.map snd fs) k.cl_props;
+    | Some (true, { CAst.v = CRecord fs; loc }) ->
+      check_duplicate ?loc fs;
       let subst, sigma =
         do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in
      let term, termtype =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index ace9096469..36c2d22c1d 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -14,12 +14,6 @@ open Constrexpr
 open Typeclasses
 open Libnames
 
-(** Errors *)
-
-val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a
-
-val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
-
 (** Instance declaration *)
 
 val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 2bc95dbfcd..9733a751a8 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -66,8 +66,6 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, sigma, te) ->
       wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te)
-  | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
-    wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
   | InductiveError e ->
       wrap_vernac_error exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a1f7835cbe..d10b704a48 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1095,19 +1095,6 @@ let explain_unbound_method env sigma cid { CAst.v = id } =
   str "Unbound method name " ++ Id.print (id) ++ spc () ++
   str"of class" ++ spc () ++ pr_global cid ++ str "."
 
-let pr_constr_exprs env sigma exprs =
-  hv 0 (List.fold_right
-         (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps)
-         exprs (mt ()))
-
-let explain_mismatched_contexts env c i j =
-  let sigma = Evd.from_env env in
-  let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in
-  str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
-    hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++
-    fnl () ++ brk (1,1) ++
-    hov 1 (str"Found:" ++ brk (1, 1) ++ pn)
-
 let explain_typeclass_error env sigma = function
   | NotAClass c -> explain_not_a_class env sigma c
   | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index d1c1c092e3..09384cb859 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -24,8 +24,6 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
 
 val explain_inductive_error : inductive_error -> Pp.t
 
-val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
-
 val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t