aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comDefinition.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comDefinition.ml')
-rw-r--r--vernac/comDefinition.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c8b289c9d..883121479 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,11 +104,11 @@ let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
-let do_definition ident k univdecl bl red_option c ctypopt hook =
+let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
let (ce, evd, univdecl, imps as def) =
interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
- if Flags.is_program_mode () then
+ if program_mode then
let env = Global.env () in
let (c,ctx), sideff = Future.force ce.const_entry_body in
assert(Safe_typing.empty_private_constants = sideff);