diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-02-25 18:44:00 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-02-28 17:26:48 +0100 |
| commit | d99fe37fc4b348fd86ac836cbe4166ef28ed34c2 (patch) | |
| tree | ff40e4dad41decdd629fb803f5006dfd066f2306 /test-suite/output/Arguments_renaming.out | |
| parent | feb82c906b62ab0f94bf57d28e10d1307a65f05f (diff) | |
Fix output test-suite 'simpl tactic' -> 'reduction tactics'
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5273c59ec..695efb260 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -55,7 +55,7 @@ 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 +The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.Test1.myplus @@ -92,7 +92,7 @@ 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 +The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus |