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.

3 files changed, 3 insertions, 28 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 3c86129fe..d967eeadf 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -251,31 +251,10 @@ let constant_context env kn =
   | Monomorphic_const _ -> Univ.AUContext.empty
   | Polymorphic_const ctx -> ctx
 
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
 
-let constant_value env (kn,u) =
-  let cb = lookup_constant kn env in
-    if cb.const_proj = None then
-      match cb.const_body with
-      | Def l_body -> 
-        begin
-          match cb.const_universes with
-          | Monomorphic_const _ -> 
-            (Mod_subst.force_constr l_body, Univ.Constraint.empty)
-          | Polymorphic_const _ ->
-	    let csts = constraints_of cb u in
-            (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
-        end
-      | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
-      | Undef _ -> raise (NotEvaluableConst NoBody)
-    else raise (NotEvaluableConst IsProj)
-
-let constant_opt_value env cst =
-  try Some (constant_value env cst)
-  with NotEvaluableConst _ -> None
-
 let constant_value_and_type env (kn, u) =
   let cb = lookup_constant kn env in
     if Declareops.constant_is_polymorphic cb then
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7cc541258..69d811a64 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 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5a522e06a..f682143f8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u =
   match evref with
   | EvalConstRef con -> 
     let u = Unsafe.to_instance u in
-    EConstr.of_constr (try constant_value_in env (con,u)
-    with NotEvaluableConst IsProj -> 
-      raise (Invalid_argument "value_of_evaluable_ref"))
+    EConstr.of_constr (constant_value_in env (con, u))
   | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get
 
 let evaluable_of_global_reference env = function