aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/cic.mli1
-rw-r--r--checker/environ.ml3
-rw-r--r--checker/environ.mli1
-rw-r--r--checker/values.ml3
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/cooking.mli1
-rw-r--r--kernel/declarations.ml1
-rw-r--r--kernel/declareops.ml1
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/term_typing.ml5
-rw-r--r--library/heads.ml2
-rw-r--r--plugins/extraction/extraction.ml4
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:08:38 +0000