diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 8a0d0c9d81..26592b5542 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -70,7 +70,7 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode - ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in + ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in (ce, evd, udecl, imps) @@ -80,7 +80,7 @@ let check_definition ~program_mode (ce, evd, _, imps) = ce let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = - let (ce, evd, univdecl, imps as def) = + let (ce, evd, univdecl, impargs as def) = interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt in if program_mode then @@ -99,10 +99,10 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o in let ctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition - ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) + ~name ~term:c cty ctx ~univdecl ~implicits:impargs ~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 let kind = Decls.IsDefinition kind in - ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) + ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs) |