diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index b3cc0a4236..3d5ea319bb 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = +let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = - interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt + interp_definition ~program_mode univdecl bl poly red_option c ctypopt in if program_mode then let env = Global.env () in @@ -95,13 +95,13 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = | None -> Retyping.get_type_of env evd c in let obls, _, c, cty = - Obligations.eterm_obligations env ident evd 0 c typ + Obligations.eterm_obligations env name evd 0 c typ in let ctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls) + ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) else let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps) + ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) |