diff options
| author | Hugo Herbelin | 2016-11-10 11:45:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-11-10 12:06:44 +0100 |
| commit | a279547e2d4e6cad75c266e4a9e436b524f5df99 (patch) | |
| tree | bf28ac6b9316b0206db53337dfca33faefce6d72 | |
| parent | 64027824d8217edbb1938394bc8a4fd4035bbf73 (diff) | |
Updating a comment in test-suite.
| -rw-r--r-- | test-suite/output/PatternsInBinders.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index fff86d6fae..6fa357a90c 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -58,7 +58,7 @@ Definition F '(n,p) : Type := (Fin n * Fin p)%type. Definition both_z '(n,p) : F (n,p) := (Z _,Z _). Print both_z. -(** These tests show examples which do not factorize binders *) +(** Test factorization of binders *) Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t). Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t). |