aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/implicit_quantifiers.ml3
-rw-r--r--interp/implicit_quantifiers.mli4
-rw-r--r--pretyping/typeclasses_errors.ml4
-rw-r--r--pretyping/typeclasses_errors.mli2
-rw-r--r--test-suite/bugs/closed/bug_10225.v7
-rw-r--r--vernac/classes.ml13
-rw-r--r--vernac/classes.mli6
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/himsg.ml13
-rw-r--r--vernac/himsg.mli2
12 files changed, 17 insertions, 47 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4c8aff3f2e..63c936fa81 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1299,7 +1299,7 @@ let find_pattern_variable qid =
if qualid_is_ident qid then qualid_basename qid
else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
-let check_duplicate loc fields =
+let check_duplicate ?loc fields =
let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
let dups = List.duplicates eq fields in
match dups with
@@ -1344,7 +1344,7 @@ let sort_fields ~complete loc fields completer =
try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
with Not_found ->
anomaly (str "Environment corruption for records.") in
- let () = check_duplicate loc fields in
+ let () = check_duplicate ?loc fields in
let (end_index, (* one past the last field index *)
first_field_index, (* index of the first field of the record *)
proj_list) (* list of projections *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d4bc91f57..2e4d7479a9 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
(** Placeholder for global option, should be moved to a parameter *)
val get_asymmetric_patterns : unit -> bool
+
+val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
+(** Check that a list of record field definitions doesn't contain
+ duplicates. *)
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*)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d28d35f3a1..8536a2dee0 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -30,7 +30,3 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t
-
-(* Should be likely located elsewhere *)
-exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
-val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index af5b3016c9..90ecab1608 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,13 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(*i*)
open Names
open EConstr
open Environ
-(*i*)
-
-type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fd75781ed5..21bb5f8443 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -12,8 +12,6 @@ open Names
open EConstr
open Environ
-type contexts = Parameters | Properties
-
type typeclass_error =
| NotAClass of constr
| UnboundMethod of GlobRef.t * lident (** Class name, method *)
diff --git a/test-suite/bugs/closed/bug_10225.v b/test-suite/bugs/closed/bug_10225.v
new file mode 100644
index 0000000000..6d6bb39a65
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10225.v
@@ -0,0 +1,7 @@
+
+Class Bar := {}.
+Instance bb : Bar := {}.
+
+Class Foo := { xx : Bar; foo : nat }.
+
+Fail Instance bar : Foo := { foo := 1 + 1; foo := 2 + 2 }.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b64af52b6e..20402ebf95 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:15:04 +0000