diff options
| author | Hugo Herbelin | 2019-01-24 21:47:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-01-24 21:47:38 +0100 |
| commit | 6994539744e4ffaa4f622c8bccc66276e445ae9a (patch) | |
| tree | 947e51227ebd55ed24b9e52b4ad1aa2b71a480cc /test-suite/output/PrintInfos.out | |
| parent | d79efa598d310b885c3472105d7d376f52dd3e50 (diff) | |
| parent | 63c7aa195022a908e0ee43d3cfb48c836405a835 (diff) | |
Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].
Reviewed-by: maximedenes
Diffstat (limited to 'test-suite/output/PrintInfos.out')
| -rw-r--r-- | test-suite/output/PrintInfos.out | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index da1fca7134..ab4172711e 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -46,7 +46,6 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add : nat -> nat -> nat @@ -86,7 +85,6 @@ Argument x is implicit and maximally inserted Expands to: Constant PrintInfos.bar *** [ bar : foo ] -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 |