diff options
| author | Théo Zimmermann | 2020-07-23 09:30:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-07-23 09:30:32 +0200 |
| commit | b8962b4d7d4c23c01b03713fcd9a0816edad3f40 (patch) | |
| tree | d0f941ef4290d74d846f68538019d32b919442a3 /dev | |
| parent | 1ea5dec77580e479885ffbea0278174fdec629fb (diff) | |
| parent | a34ba68fd83f6044da3255c4a0f91c141aafceda (diff) | |
Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a qualid in tactic notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions