diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 3 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 4 |
4 files changed, 6 insertions, 9 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 |