diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 263ebf5f5a..4664df3182 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id if program_mode then let hook _ _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr [imps]; + Impargs.declare_manual_implicits false gr imps; let pri = intern_info pri in Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst) in @@ -234,7 +234,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct in match rest with | (n, _) :: _ -> - unbound_method env' k.cl_impl (get_id n) + unbound_method env' sigma k.cl_impl (get_id n) | _ -> let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in |