diff options
| author | Matthieu Sozeau | 2013-10-11 18:30:54 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:53 +0200 |
| commit | 57bee17f928fc67a599d2116edb42a59eeb21477 (patch) | |
| tree | f8e1446f5869de08be1dc20c104d61d0e47ce57d /kernel | |
| 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 'kernel')
| -rw-r--r-- | kernel/entries.mli | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 8 |
3 files changed, 7 insertions, 7 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index 24e029bc09..1bc3bbd15b 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -62,8 +62,8 @@ type definition_entry = { const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_polymorphic : bool; - const_entry_universes : Univ.universe_context; - const_entry_proj : projection option; + const_entry_universes : Univ.universe_context Future.computation; + const_entry_proj : projection option; const_entry_opaque : bool; const_entry_inline_code : bool } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 093797fc05..7d49e452c9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -301,7 +301,7 @@ let push_named_def (id,de) senv = | Def c -> Mod_subst.force_constr c | OpaqueDef o -> Opaqueproof.force_proof o | _ -> assert false in - let senv' = push_context de.Entries.const_entry_universes senv in + let senv' = push_context (Future.join de.Entries.const_entry_universes) senv in let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9aa688fc71..352ef40d90 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -101,7 +101,7 @@ let infer_declaration env kn dcl = Undef nl, t, None, poly, Future.from_val uctx, false, ctx | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true } as c) -> - let env = push_context c.const_entry_universes env in + let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *) let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -113,10 +113,10 @@ let infer_declaration env kn dcl = feedback_completion_typecheck feedback_id; j.uj_val, Univ.empty_constraint) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, typ, None, c.const_entry_polymorphic, Future.from_val c.const_entry_universes, + def, typ, None, c.const_entry_polymorphic, c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx | DefinitionEntry c -> - let env = push_context c.const_entry_universes env in + let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *) let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let body, side_eff = Future.join body in @@ -127,7 +127,7 @@ let infer_declaration env kn dcl = feedback_completion_typecheck feedback_id; let def = Def (Mod_subst.from_val j.uj_val) in def, typ, None, c.const_entry_polymorphic, - Future.from_val c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx + c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx (* let global_vars_set_constant_type env = function *) (* | NonPolymorphicType t -> global_vars_set env t *) |