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.out | |
| parent | b5a5253d90275c373c15ff1dd384fea98fe714fd (diff) | |
Fixing clash in output test-suite Cases.
Diffstat (limited to 'test-suite/output/Cases.out')
| -rw-r--r-- | test-suite/output/Cases.out | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 0ebc251bc..d59034836 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -8,14 +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 + = fun d : TT => match d with + | @CTT _ _ b => b + end + : TT -> 0 = 0 + = fun d : TT => match d with + | @CTT _ _ b => b + end + : TT -> 0 = 0 proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with |