diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-11 18:30:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:53 +0200 |
| commit | 57bee17f928fc67a599d2116edb42a59eeb21477 (patch) | |
| tree | f8e1446f5869de08be1dc20c104d61d0e47ce57d /toplevel/class.ml | |
| parent | a4043608f704f026de7eb5167a109ca48e00c221 (diff) | |
Rework handling of universes on top of the STM, allowing for delayed
computation in case of non-polymorphic proofs. Also fix plugins after
forgotten merge conflicts. Still does not compile everything.
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index d54efb632..eedb35acf 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -217,17 +217,9 @@ let build_id_coercion idf_opt source poly = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - { const_entry_body = Future.from_val - (mkCast (val_f, DEFAULTcast, typ_f),Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = Some typ_f; - const_entry_proj = None; - const_entry_polymorphic = poly; - const_entry_universes = Univ.ContextSet.to_context ctx; - const_entry_opaque = false; - const_entry_inline_code = true; - const_entry_feedback = None; - } in + (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx) + ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) + in let decl = (constr_entry, IsDefinition IdentityCoercion) in let kn = declare_constant idf decl in ConstRef kn |