diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 39c086eff5..1981e24ae4 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 @@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in obls, Some constr, typ | None -> [||], None, termtype in - let univ_hook = Obligations.mk_univ_hook hook in + let hook = Lemmas.mk_hook hook in let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls) + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) else Flags.silently (fun () -> (* spiwack: it is hard to reorder the actions to do @@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id let sigma = Evd.reset_future_goals sigma in Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) ~hook:(Lemmas.mk_hook - (fun _ -> instance_hook k pri global imps ?hook)); + (fun _ _ _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then let init_refine = @@ -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 @@ -352,8 +352,8 @@ let named_of_rel_context l = (fun decl (subst, ctx) -> let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in let d = match decl with - | LocalAssum (_,t) -> id, None, substl subst t - | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in + | LocalAssum (_,t) -> id, None, substl subst t + | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in (mkVar id :: subst, d :: ctx)) l ([], []) in ctx |