Use projection opacity for compat. constant opacity in evarconv.ml

coq · Dec 8, 2023 · 8a8a22c · 8a8a22c
1 parent 2f55506
commit 8a8a22c
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
@@ -79,7 +79,12 @@ let unfold_projection env evd ts p r c =
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
   | Const (c, u) ->
-      if TransparentState.is_transparent_constant ts c
+      let transparent =
+        match Structures.PrimitiveProjections.find_opt c with
+        | Some pr -> TransparentState.is_transparent_projection ts pr
+        | None -> TransparentState.is_transparent_constant ts c
+      in
+      if transparent
       then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
       else None
   | Rel n ->