diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 18:10:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 18:46:27 +0200 |
| commit | 20eb7fed88ec3154721e34b549e39c0b5cefba23 (patch) | |
| tree | 6848b067d262e0a20f84e49adf795021037b42e3 /test-suite/output/Cases.v | |
| parent | b5a5253d90275c373c15ff1dd384fea98fe714fd (diff) | |
Fixing clash in output test-suite Cases.
Diffstat (limited to 'test-suite/output/Cases.v')
| -rw-r--r-- | test-suite/output/Cases.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index ef3a3a71e..4116a5ebc 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -5,10 +5,10 @@ Inductive t : Set := Print t_rect. -Record A : Type := C { a := 0 : nat; c: nat; b : a=a }. +Record TT : Type := CTT { f1 := 0 : nat; f2: nat; f3 : f1=f1 }. -Eval cbv in fun d:A => match d return 0 = 0 with C a _ b => b end. -Eval lazy in fun d:A => match d return 0 = 0 with C a _ b => b end. +Eval cbv in fun d:TT => match d return 0 = 0 with CTT a _ b => b end. +Eval lazy in fun d:TT => match d return 0 = 0 with CTT a _ b => b end. (* Do not contract nested patterns with dependent return type *) (* see bug #1699 *) |