From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 1 Jun 2018 16:23:29 +0200
Subject: 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.
---
 kernel/cooking.ml      | 2 --
 kernel/cooking.mli     | 1 -
 kernel/declarations.ml | 1 -
 kernel/declareops.ml   | 1 -
 kernel/environ.ml      | 2 +-
 kernel/term_typing.ml  | 5 -----
 6 files changed, 1 insertion(+), 11 deletions(-)

(limited to 'kernel')

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;
-- 
cgit v1.2.3