diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-01 16:23:29 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-17 11:34:43 +0200 |
commit | 74d700e9f7fcb14e7136e87b5efab25d5adb194b (patch) | |
tree | 6b5c575b669a385931e61c645d137dc356985a77 /kernel | |
parent | d62354b7e9ff8e20aa959984b392a27e26f9fc24 (diff) |
Getting rid of the const_proj field in the kernel.
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cooking.ml | 2 | ||||
-rw-r--r-- | kernel/cooking.mli | 1 | ||||
-rw-r--r-- | kernel/declarations.ml | 1 | ||||
-rw-r--r-- | kernel/declareops.ml | 1 | ||||
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/term_typing.ml | 5 |
6 files changed, 1 insertions, 11 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5783453e6..68057b389 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -230,7 +229,6 @@ let cook_constant ~hcons env { from = cb; info } = { cook_body = body; cook_type = typ; - cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0d907f3de..76c79335f 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd70c050..02871153b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,7 +87,6 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 75c0e5b4c..fc6dc8b9e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -100,7 +100,6 @@ let subst_const_body sub cb = { const_hyps = []; const_body = body'; const_type = type'; - const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/environ.ml b/kernel/environ.ml index fb89576dd..2d6c9117b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -490,7 +490,7 @@ let lookup_projection cst env = Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - (lookup_constant cst env).const_proj + Cmap_env.mem cst env.env_globals.env_projections (* Mutual Inductives *) let polymorphic_ind (mind,i) env = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index db1109e75..d29f2ca82 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,7 +341,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +367,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; - cook_proj = true; cook_universes = univs; cook_inline = false; cook_context = None; @@ -464,7 +460,6 @@ let build_constant_declaration kn env result = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; const_inline_code = result.cook_inline; |