diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /test-suite/output/PrintInfos.out | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'test-suite/output/PrintInfos.out')
-rw-r--r-- | test-suite/output/PrintInfos.out | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 0457c860..ba076f05 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -25,7 +25,6 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x -eq_refl is not universe polymorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -46,11 +45,9 @@ 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 -Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add is transparent Expands to: Constant Coq.Init.Nat.add @@ -58,7 +55,6 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 -plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O @@ -80,13 +76,11 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set -comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -94,14 +88,12 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted bar : foo -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -109,7 +101,6 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 |