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.

12 files changed, 5 insertions, 21 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 7ec345768..5543e5720 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -241,7 +241,6 @@ type constant_body = {
     const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
-    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags;
 }
diff --git a/checker/environ.ml b/checker/environ.ml
index 809150cea..3d5fac806 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -166,9 +166,6 @@ let evaluable_constant cst env =
   try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
-let is_projection cst env = 
-  (lookup_constant cst env).const_proj
-
 let lookup_projection p env =
   Cmap_env.find (Projection.constant p) env.env_globals.env_projections
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 4a7597249..acb29d7d2 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : Constant.t -> env -> bool
 val lookup_projection : Projection.t -> env -> projection_body
 
 (* Inductives *)
diff --git a/checker/values.ml b/checker/values.ml
index 67032bd1b..f1c4fd470 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
+MD5 3d9612f0adc70404fddb093b85c7d168 checker/cic.mli
 
 *)
 
@@ -241,7 +241,6 @@ let v_cb = v_tuple "constant_body"
     Any;
     v_const_univs;
     v_bool;
-    v_bool;
     v_typing_flags|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
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;
diff --git a/library/heads.ml b/library/heads.ml
index 3d5f6a6ff..d9d650ac0 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
    let cb = Environ.lookup_constant cst env in
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
-     if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body
+     if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body
      then Global.body_of_constant cst else None
    in
      (match body with
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5aee70194..b1ee21536 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1065,7 +1065,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
@@ -1078,7 +1078,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in