diff options
| author | Hugo Herbelin | 2014-05-08 21:38:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-05-08 21:38:28 +0200 |
| commit | f3387bed0eed592ab857ef36db8dcca34843d63e (patch) | |
| tree | b6f4dda0db9a2c82f7da06c2ee74d84d576ced9a /kernel | |
| parent | b797ba85b7b0f82d66af5629ccf6f75d90dda99a (diff) | |
Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."
(made push command with wrong local ref; leaving control to Matthieu
on new revert)
This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions