diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 10:11:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 10:52:19 +0100 |
| commit | 1de1d505dfd1c5a05a4910cfc872971087de26fb (patch) | |
| tree | e276f4cbf43d9bc2a95ace51b86111852b1f53c4 /kernel/safe_typing.ml | |
| parent | c3e26fca1d077a2b69926df85d05e067882c40b0 (diff) | |
Let definitions do not create new universe constraints.
We force the upper layers to extrude the universe constraints before sending
it to the kernel. This simplifies the suspicious handling of polymorphic
constraints for section-local definitions.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 19 |
1 files changed, 3 insertions, 16 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 4fbe02cf5..93b8e278f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,22 +382,9 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let open Entries in - let c,typ,univs = Term_typing.translate_local_def senv.env id de in - let poly = match de.Entries.secdef_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true - in - let c, univs = match c with - | Def c -> Mod_subst.force_constr c, univs - | OpaqueDef o -> - Opaqueproof.force_proof (Environ.opaque_tables senv.env) o, - Univ.ContextSet.union univs - (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o) - | _ -> assert false in - let senv' = push_context_set poly univs senv in - let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in - univs, {senv' with env=env''} + let c, typ = Term_typing.translate_local_def senv.env id de in + let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in + { senv with env = env'' } let push_named_assum ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in |