diff options
| author | Hugo Herbelin | 2014-09-07 13:08:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-07 13:52:47 +0200 |
| commit | 62fa2039ca0fc162af31e06bf586e8e5df005455 (patch) | |
| tree | 875e1da0a409ae0baf39547fe28861a7e197986a /plugins/pluginsbyte.itarget | |
| parent | 69665dd2480d364162933972de7ffa955eccab4d (diff) | |
A better check that an "as" clause has been given to inversion, so
that it clears things earlier in the "as" case, allowing
intros_replacing to work without renaming the hypotheses.
(clear_request was not a good idea here a priori, since its use was
not related to the hypothesis to invert but to an hypothesis to inject).
Diffstat (limited to 'plugins/pluginsbyte.itarget')
0 files changed, 0 insertions, 0 deletions