diff options
Diffstat (limited to 'test-suite/output/Arguments.out')
| -rw-r--r-- | test-suite/output/Arguments.out | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 6704337f80..f889da4e98 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,7 +1,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch +Arguments Nat.sub (_ _)%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub @@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub !_%nat_scope !_%nat_scope / +Arguments Nat.sub (!_ !_)%nat_scope / The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent @@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub !_%nat_scope !_%nat_scope +Arguments Nat.sub (!_ !_)%nat_scope The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor Nat.sub is transparent @@ -43,14 +43,14 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never +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 is not universe polymorphic -Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / +Arguments fcomp {A B C}%type_scope _ _ _ / The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp @@ -78,7 +78,7 @@ Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent @@ -86,7 +86,7 @@ Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent |