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 /vernac/classes.ml | |
| parent | c0e5746e6b273eb4592d24867da55dde40b656c9 (diff) | |
| parent | 1e1d8d67442dc3cdd248b7f5e027b9d6bf998ba3 (diff) | |
Merge PR #6405: Remove the local polymorphic flag hack.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 6914f899b7..4a2dba859f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -69,8 +69,7 @@ let existing_instance glob g info = let instance, _ = Global.type_of_global_in_context (Global.env ()) c in let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with - | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob - (*FIXME*) (Flags.use_polymorphic_flag ()) c) + | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) | None -> user_err ?loc:(loc_of_reference g) ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -393,8 +392,7 @@ let context poly l = let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr sigma (of_constr t) with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*) - poly (ConstRef cst)); + add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst)); status (* declare_subclasses (ConstRef cst) cl *) | None -> status |