From cff295c4bbc796c4d838842795c324601a2a037c Mon Sep 17 00:00:00 2001
From: Andreas Lynge
Date: Fri, 30 Aug 2019 10:58:42 +0200
Subject: Make SSR congr tactic work on arrows in Type.

Matthieu Sozeau explained how to fix this.
---
 test-suite/ssr/congr.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v
index 026f7538e8..f85791b00b 100644
--- a/test-suite/ssr/congr.v
+++ b/test-suite/ssr/congr.v
@@ -32,3 +32,11 @@ Coercion f : nat >-> Equality.sort.
 
 Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a).
 Proof. move=> a b Eba; congr (_ + _); exact:  Eba. Qed.
+
+Open Scope type_scope.
+
+Lemma test5 : forall (P Q Q' : Type) (h : Q = Q'), P * Q = P * Q'.
+Proof. move=>*; by congr (_ * _). Qed.
+
+Lemma test6 : forall (P Q Q' : Type) (h : Q = Q'), P * Q -> P * Q'.
+Proof. move=> P Q Q' h; by congr (_ * _). Qed.
-- 
cgit v1.2.3