diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index e4064049e..a217abbba 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -103,7 +103,7 @@ let instance_hook k pri global imps ?hook cst = let declare_instance_constant k pri global imps ?hook id term termtype = let kind = IsDefinition Instance in let entry = { - const_entry_body = term; + const_entry_body = Future.from_val term; const_entry_secctx = None; const_entry_type = Some termtype; const_entry_opaque = false; @@ -273,7 +273,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let evm = Evarutil.nf_evar_map_undefined !evars in let evm = undefined_evars evm in if Evd.is_empty evm && not (Option.is_empty term) then - declare_instance_constant k pri global imps ?hook id (Option.get term) termtype + declare_instance_constant k pri global imps ?hook id + (Option.get term,Declareops.no_seff) termtype else begin let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in if Flags.is_program_mode () then |