diff options
| author | Pierre-Marie Pédrot | 2020-11-29 17:29:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-29 17:29:15 +0100 |
| commit | ca8ee04a692e14bd90c64113ff29b7df1d5111bd (patch) | |
| tree | f5149acae95edbd1baf8de064bb716f4e84cd5f2 /test-suite | |
| parent | 9992bb15d4f90fc0cf3aa2854beb209bc5effac6 (diff) | |
| parent | 223c86e91a4c5dceb8bdacf411f47c43d69a5dd0 (diff) | |
Merge PR #13514: Fixing printing of apply in (continuation of #12246)
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Tactics.out | 1 | ||||
| -rw-r--r-- | test-suite/output/Tactics.v | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 3f07261ca6..01bf727ebc 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -9,3 +9,4 @@ H is already used. a The command has indeed failed with message: This variable is used in hypothesis H. +Ltac test a b c d e := apply a, b in c as [], d, e as -> diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 8526e43a23..845bccc548 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -38,3 +38,10 @@ Fail intros ((n,_),H). Abort. End IntroWildcard. + +Module ApplyIn. + +Ltac test a b c d e := apply a, b in c as [], d, e as ->. +Print test. + +End ApplyIn. |