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/Implicit.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/Implicit.out')
| -rw-r--r-- | test-suite/output/Implicit.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index d1cd5e84f..0b0f501f9 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -d2 is monomorphic +d2 is not universe polymorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) |