diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Arguments.out | 25 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 8 |
2 files changed, 16 insertions, 17 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7c9b1e27cf..f5636fbf9d 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -22,16 +22,15 @@ Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor and - when applied to 2 arguments +The simpl tactic unfolds minus when the 1st and + 2nd arguments evaluate to a constructor and when applied to 2 arguments minus is transparent Expands to: Constant Coq.Init.Peano.minus minus : nat -> nat -> nat Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor +The simpl tactic unfolds minus when the 1st and + 2nd arguments evaluate to a constructor minus is transparent Expands to: Constant Coq.Init.Peano.minus pf : @@ -65,30 +64,30 @@ Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat Argument scopes are [_ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 3rd, 4th and 5th arguments evaluate to a constructor +The simpl tactic unfolds f when the 3rd, 4th and + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 4th, 5th and 6th arguments evaluate to a constructor +The simpl tactic unfolds f when the 4th, 5th and + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +The simpl tactic unfolds f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +The simpl tactic unfolds f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f forall w : r, w 3 true = tt diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e443115cb3..20042a5ed0 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -53,8 +53,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The simpl tactic unfolds myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.Test1.myplus myplus @@ -90,8 +90,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The simpl tactic unfolds myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus myplus |