diff options
| author | Enrico Tassi | 2019-09-02 15:53:41 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-09-02 15:53:41 +0200 |
| commit | 671bc2bba6576434bee3be5e0b45d4f1515c7443 (patch) | |
| tree | ad0584aedaeb88c439f3d55d857c666f1e0526ec /test-suite | |
| parent | 61750abbc38dee8f9299b309979e0382d48ac323 (diff) | |
| parent | cff295c4bbc796c4d838842795c324601a2a037c (diff) | |
Merge PR #10719: Make SSR congr tactic work on arrows in Type.
Reviewed-by: gares
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/congr.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |