Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for primitive projections

2 files changed, 12 insertions, 14 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index 3830cd0dc2..bbd043c8e9 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -126,7 +126,7 @@ let add_constant kn cs env =
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
 
 (* Constant types *)
 
@@ -148,18 +148,16 @@ 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 -> 
-      let b = force_constr l_body in
-      begin
-        match cb.const_universes with
-        | Monomorphic_const _ -> b
-        | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
-      end
-    | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
-    | Undef _ -> raise (NotEvaluableConst NoBody)
-  else raise (NotEvaluableConst IsProj)
+  match cb.const_body with
+  | Def l_body ->
+    let b = force_constr l_body in
+    begin
+      match cb.const_universes with
+      | Monomorphic_const _ -> b
+      | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+    end
+  | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+  | Undef _ -> raise (NotEvaluableConst NoBody)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index ba62ed519b..36e0ea0274 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -52,7 +52,7 @@ val check_constraints : Univ.constraints -> env -> bool
 val lookup_constant : Constant.t -> env -> Cic.constant_body
 val add_constant : Constant.t -> Cic.constant_body -> env -> env
 val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
-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
 val evaluable_constant : Constant.t -> env -> bool