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

6 files changed, 25 insertions, 42 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index 3830cd0dc..bbd043c8e 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 ba62ed519..36e0ea027 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
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 93dc2f9a7..738ecc6e1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -254,31 +254,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
diff --git a/test-suite/coqchk/primproj2.v b/test-suite/coqchk/primproj2.v
new file mode 100644
index 000000000..f73c627ee
--- /dev/null
+++ b/test-suite/coqchk/primproj2.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+Record Pack (A : Type) := pack { unpack : A }.
+
+Definition p : Pack bool.
+Proof.
+refine (pack _ true).
+Qed.
+
+Definition boom : unpack bool p = let u := unpack _ in u p := eq_refl.