diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 11:33:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 13:37:14 +0200 |
| commit | c7480636bce632adfa28d6bb0b423a086ade4318 (patch) | |
| tree | 24fbca8dbed1d873064ce2a2473947a6d10e17d6 /test-suite/output/ArgumentsScope.out | |
| parent | c0316d627b80b1e81fc020762f835a1695966a64 (diff) | |
Upgrading output tests.
output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v
Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
Diffstat (limited to 'test-suite/output/ArgumentsScope.out')
| -rw-r--r-- | test-suite/output/ArgumentsScope.out | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 358a96bc3..71d5fc78b 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,70 +1,70 @@ a : bool -> bool -a is monomorphic +a is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool -b is monomorphic +b is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool -negb'' is monomorphic +negb'' is not universe polymorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant Top.A.B.negb'' negb' : bool -> bool -negb' is monomorphic +negb' is not universe polymorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant Top.A.negb' negb : bool -> bool -negb is monomorphic +negb is not universe polymorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool -a is monomorphic +a is not universe polymorphic Expands to: Variable a b : bool -> bool -b is monomorphic +b is not universe polymorphic Expands to: Variable b negb : bool -> bool -negb is monomorphic +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool -negb' is monomorphic +negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.A.negb' negb'' : bool -> bool -negb'' is monomorphic +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.A.B.negb'' a : bool -> bool -a is monomorphic +a is not universe polymorphic Expands to: Variable a negb : bool -> bool -negb is monomorphic +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool -negb' is monomorphic +negb' is not universe polymorphic negb' is transparent Expands to: Constant Top.negb' negb'' : bool -> bool -negb'' is monomorphic +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant Top.negb'' |