diff options
| author | Emilio Jesus Gallego Arias | 2018-04-08 09:35:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:22:50 +0100 |
| commit | 7efaf86882488034e6545505e1eda7d6e1a6ce14 (patch) | |
| tree | 7a0aafae5d81a510877489500ffa434763315a51 /vernac/comDefinition.ml | |
| parent | 54a2a3a07e14c597b264566e01d2ecc69c4bd90c (diff) | |
[vernac] Adapt to removal of imperative proof state.
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) |