diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 15:31:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 15:35:59 +0200 |
| commit | 0cebd2b86a90cc1361bcfac6bb097540e22c9a21 (patch) | |
| tree | 648ece59fd72185da10d71771d9f858aa1fa7fd4 /test-suite/output/Implicit.out | |
| parent | 6a3767e48e91604071b5709a6658aa2f255a4522 (diff) | |
Fixing output test-suite: since universe polymorphism, the Print command
shows the polymorphism status of the term.
Diffstat (limited to 'test-suite/output/Implicit.out')
| -rw-r--r-- | test-suite/output/Implicit.out | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c2..d1cd5e84f 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,6 +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 Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) |