From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot 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. --- checker/cic.mli | 1 - checker/environ.ml | 3 --- checker/environ.mli | 1 - checker/values.ml | 3 +-- 4 files changed, 1 insertion(+), 7 deletions(-) (limited to 'checker') 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 *) -- cgit v1.2.3