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 /library | |
| 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 'library')
| -rw-r--r-- | library/declare.ml | 14 | ||||
| -rw-r--r-- | library/declare.mli | 4 |
2 files changed, 9 insertions, 9 deletions
diff --git a/library/declare.ml b/library/declare.ml index 452504bf0..41f50753f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -64,7 +64,7 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let () = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, - (Univ.ContextSet.of_context de.const_entry_universes) in + (Univ.ContextSet.of_context (Future.force de.const_entry_universes)) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; @@ -194,17 +194,17 @@ let declare_constant_common id cst = Notation.declare_ref_arguments_scope (ConstRef c); c -let definition_entry ?(opaque=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) body = - { const_entry_body = Future.from_val (body,Declareops.no_seff); +let definition_entry ?(opaque=false) ?(inline=false) ?types + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = + { const_entry_body = Future.from_val (body,eff); const_entry_secctx = None; const_entry_type = types; const_entry_proj = None; const_entry_polymorphic = poly; - const_entry_universes = univs; + const_entry_universes = Future.from_val univs; const_entry_opaque = opaque; const_entry_feedback = None; - const_entry_inline_code = false} + const_entry_inline_code = inline} let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f @@ -234,7 +234,7 @@ let declare_sideff se = const_entry_inline_code = false; const_entry_feedback = None; const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = Future.join cb.const_universes; + const_entry_universes = cb.const_universes; const_entry_proj = None; }); cst_hyps = [] ; diff --git a/library/declare.mli b/library/declare.mli index 848bab618..ed3e4dcc3 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -48,8 +48,8 @@ type internal_flag = | UserVerbose (* Defaut definition entries, transparent with no secctx or proj information *) -val definition_entry : ?opaque:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> +val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> + ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> constr -> definition_entry val declare_constant : |