Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index bbfe5ec4..49a8b9cf 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -151,3 +151,17 @@ Section JLeivant.
     congruence.
   Qed.
 End JLeivant.
+
+(* An example with primitive projections *)
+
+Module PrimitiveProjections.
+Set Primitive Projections.
+Record t (A:Type) := { f : A }.
+Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0.
+congruence.
+Undo.
+intros.
+unfold f in H0. (* internally turn the projection to unfolded form *)
+congruence.
+Qed.
+End PrimitiveProjections.