diff options
| author | Pierre-Marie Pédrot | 2018-11-12 17:34:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-12 17:34:14 +0100 |
| commit | b42e67e8a5afd9eee49c813fedc016904fcdc10f (patch) | |
| tree | 29a8056b017df8b1e900024304f4893defba2ae2 /vernac | |
| parent | 040fdec17f7e70fdbef7d400be2dc0e1607a10fa (diff) | |
| parent | ccefe52e6cb755da9470ef1fe707d570a26681cb (diff) | |
Merge PR #8972: Fix #4771: Substitution of inline global reference in tactics is broken
Diffstat (limited to 'vernac')
0 files changed, 0 insertions, 0 deletions