diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-02 15:11:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-17 11:44:00 +0200 |
| commit | 4513b7735779fb440223e6f22079994528249047 (patch) | |
| tree | 101660d2dd2f1788d49c4b45ee4d62d7d142ebc2 /kernel/term_typing.ml | |
| parent | 74d700e9f7fcb14e7136e87b5efab25d5adb194b (diff) | |
Remove special declaration of primitive projections in the kernel.
This reduces kernel bloat and removes code from the TCB, as compatibility
projections are now retypechecked as normal definitions would have been.
This should have no effect on efficiency as this only happens once at
definition time.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d29f2ca82..37bf679c5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -346,32 +346,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } - | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> - let mib, _ = Inductive.lookup_mind_specif env (ind,0) in - let kn, pb = - match mib.mind_record with - | Some (Some (id, kns, pbs)) -> - if i < Array.length pbs then - kns.(i), pbs.(i) - else assert false - | _ -> assert false - in - let univs = - match mib.mind_universes with - | Monomorphic_ind ctx -> Monomorphic_const ctx - | Polymorphic_ind auctx -> Polymorphic_const auctx - | Cumulative_ind acumi -> - Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) - in - let term, typ = pb.proj_eta in - { - Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); - cook_type = typ; - cook_universes = univs; - cook_inline = false; - cook_context = None; - } - let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = |