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/environ.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'checker/environ.mli') 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 *) -- cgit v1.2.3