diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index c2e9a5ab44..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.") @@ -141,7 +140,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false (fun avoid (clname, _) -> match clname with - | Some (cl, b) -> + | Some cl -> let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in t, avoid | None -> failwith ("new instance: under-applied typeclass")) @@ -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 |