diff options
| author | Hugo Herbelin | 2015-11-08 09:47:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-08 09:56:05 +0100 |
| commit | b382bb1b42319d7be422f92fd196df8bfbe21a83 (patch) | |
| tree | 48e213fc660764237a2a069d48760d1fca7d1655 | |
| parent | a593bb93b3047986bf9ac335ab21530621962885 (diff) | |
Adapting output test inference.v after c23f0cab6 (experimenting
printing the type of the defined term of a LetIn).
| -rw-r--r-- | test-suite/output/inference.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index f2d1447785..c5a393408e 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,7 +6,7 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n in ?y ?y0 : T n +fun n : nat => let x := A n : T n in ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat x := A n : T n |- ?T0 -> T n] |