Restore original behavior of is_neutral on prim. projections

coq · Dec 12, 2023 · 974201f · 974201f
1 parent d1b0976
commit 974201f
Showing 1 changed file with 1 addition and 5 deletions.
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
@@ -648,11 +648,7 @@ let rec is_neutral env sigma ts t =
     | Rel n -> true
     | Evar _ | Meta _ -> true
     | Case (_, _, _, _, _, c, _) -> is_neutral env sigma ts c
-    | Proj (p, _, c) ->
-      let rp = Projection.repr p in
-      (not (is_transparent env (Evaluable.EvalProjectionRef rp)) ||
-       not (TransparentState.is_transparent_projection ts rp)) &&
-      is_neutral env sigma ts c
+    | Proj (p, _, c) -> is_neutral env sigma ts c
     | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false
     | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
     | Fix _ -> false (* This is an approximation *)