From f77b88a498f7e64bc35ade6fa74a00c2550bdf7f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 20 Jan 2018 22:59:48 +0100
Subject: Remove dead code in Environ.

The constant_value function was actually not behaving the same as
constant_value_in w.r.t. projections. The former was not used, and
the only place that used the latter was in Tacred and was statically
insensitive to the use of projections.
---
 kernel/environ.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7cc541258d..69d811a642 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -146,13 +146,11 @@ val type_in_type_constant : Constant.t -> env -> bool
    body and [NotEvaluableConst IsProj] if [c] is a projection 
    and [Not_found] if it does not exist in [env] *)
 
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 
-val constant_value : env -> Constant.t puniverses -> constr constrained
 val constant_type : env -> Constant.t puniverses -> types constrained
 
-val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option
 val constant_value_and_type : env -> Constant.t puniverses -> 
   constr option * types * Univ.Constraint.t
 (** The universe context associated to the constant, empty if not 
-- 
cgit v1.2.3