aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2089bc944..898ef0d9e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id pl
poly evm (Option.get term) termtype
- else if !refine_instance || Option.is_empty term then begin
+ else if Flags.is_program_mode () || !refine_instance || Option.is_empty term then begin
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if Flags.is_program_mode () then
let hook vis gr _ =