diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 28773a3965..feaf47df18 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ 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 ~ontop ~program_mode ?hook ident k 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 in @@ -114,4 +114,4 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = 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 ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps) |