diff options
| author | Andreas Lynge | 2019-08-30 10:58:42 +0200 |
|---|---|---|
| committer | Andreas Lynge | 2019-08-30 12:21:59 +0200 |
| commit | cff295c4bbc796c4d838842795c324601a2a037c (patch) | |
| tree | 90c73e563edf1bf9bf6feb8ca4596e4f9d67da10 /test-suite | |
| parent | 38aa59e1aa2edeca7dabe4275790295559751e72 (diff) | |
Make SSR congr tactic work on arrows in Type.
Matthieu Sozeau explained how to fix this.
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. |