diff options
| author | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
| commit | b3081e0906e7096e5b1aef3d5a865881d660c917 (patch) | |
| tree | bc919a6b43f27d02f30fa13f5922362f723eedff /dev/include | |
| parent | c5353cb7118690f7ea5e4a1ac3c02448424b8c03 (diff) | |
Revert "When interpreting "match goal with ... end" in ltac, expand evars by"
This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions