diff options
| author | SimonBoulier | 2020-03-18 11:15:15 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-03-18 11:15:15 +0100 |
| commit | ea16c402392722a44bf2227aef7ff73faef70d3a (patch) | |
| tree | 6d0373f5e73a235b6e9a348e9b13edd0b76acc8c /test-suite/output/Arguments.out | |
| parent | 0626df49c72badbb51d2f31eb7d1b1fee22c2638 (diff) | |
Change some ouput tests due to the printing of implicits
Diffstat (limited to 'test-suite/output/Arguments.out')
| -rw-r--r-- | test-suite/output/Arguments.out | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index f889da4e98..8cf0797b17 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -39,7 +39,7 @@ The reduction tactics unfold Nat.sub when the 1st and Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : -forall D1 C1 : Type, +forall {D1 C1 : Type}, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic @@ -47,7 +47,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf -fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments fcomp {A B C}%type_scope _ _ _ / @@ -75,7 +75,7 @@ The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f -f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope @@ -83,7 +83,7 @@ The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f -f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope |