diff options
| author | Pierre-Marie Pédrot | 2014-09-04 12:09:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 12:57:32 +0200 |
| commit | ba9ba59be9534b42ede74adfcbf8b85b876590c7 (patch) | |
| tree | 13968dc5748fd57edf40e606e96767dcedc5a31c /doc/stdlib | |
| parent | 85f440deb8b87fe42a3623bbafd1f78243711a34 (diff) | |
Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."
This reverts commit afa441019432f70245fed6adc5eb0318514e4357.
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions