diff options
| author | Maxime Dénès | 2017-12-29 13:43:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-29 13:43:28 +0100 |
| commit | 3624d943513ff1d79fdadf5b231ffcd3786b16c8 (patch) | |
| tree | 6bfd3884ff693eb7bfe5abd3dfc21c537eb5f1ea /pretyping | |
| parent | c0e5746e6b273eb4592d24867da55dde40b656c9 (diff) | |
| parent | 1e1d8d67442dc3cdd248b7f5e027b9d6bf998ba3 (diff) | |
Merge PR #6405: Remove the local polymorphic flag hack.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 2 |
2 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bc9990d026..f153b63410 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -87,7 +87,6 @@ type instance = { (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_poly: bool; is_impl: global_reference; } @@ -97,7 +96,7 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl info glob poly impl = +let new_instance cl info glob impl = let global = if glob then Some (Lib.sections_depth ()) else None @@ -107,7 +106,6 @@ let new_instance cl info glob poly impl = { is_class = cl.cl_impl; is_info = info ; is_global = global ; - is_poly = poly; is_impl = impl } (* @@ -420,7 +418,7 @@ let declare_instance info local glob = match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); - add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) + add_instance (new_instance tc info (not local) glob) | None -> () let add_class cl = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 0cbe1c71c0..ee28ec173b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -53,7 +53,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit |