diff options
| author | Hugo Herbelin | 2014-10-20 12:56:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-20 23:29:19 +0200 |
| commit | 7efeff178470ab204e531cd07176091bf5022da6 (patch) | |
| tree | afdc79d6eb2a371fa2cec235aabea3c5425d46b9 /test-suite | |
| parent | f00f8482e1d21ef8b03044ed2162cb29d9e4537d (diff) | |
A patch for printing "match" when constructors are defined with let-in
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Cases.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Cases.v | 5 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index c768f09cea..0ebc251bcd 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -8,6 +8,14 @@ fix F (t : t) : P t := (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t t_rect is not universe polymorphic + = fun d : A => match d with + | @C _ _ b => b + end + : A -> 0 = 0 + = fun d : A => match d with + | @C _ _ b => b + end + : A -> 0 = 0 proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 30ef8778d3..ef3a3a71e4 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -5,6 +5,11 @@ Inductive t : Set := Print t_rect. +Record A : Type := C { a := 0 : nat; c: nat; b : a=a }. + +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. + (* Do not contract nested patterns with dependent return type *) (* see bug #1699 *) |