diff options
Diffstat (limited to 'contrib/subtac/subtac_classes.ml')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 2a8e2e5d9..7ec5d3575 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -100,7 +100,7 @@ let type_class_instance_params isevars env id n ctx inst subst = let substitution_of_constrs ctx cstrs = List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] -let new_instance ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = +let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in @@ -204,12 +204,7 @@ let new_instance ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_fr (* 1 ctx *) (* in *) let hook cst = - let inst = - { is_class = k; - is_pri = pri; - is_impl = cst; - } - in + let inst = Typeclasses.new_instance k pri global cst in Impargs.declare_manual_implicits false (ConstRef cst) false imps; Typeclasses.add_instance inst in |