diff options
| author | Gaëtan Gilbert | 2019-11-28 19:18:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-28 19:21:06 +0100 |
| commit | d9a0cdc557d2c8b94b9fe2f8b78eacf8be4f77f9 (patch) | |
| tree | 5d9412bff5fafea014eadf8aa7af5e48eb6e715e /dev | |
| parent | fc5fa8ffafcb0c1e3e0afcc414dfa14f7c85b6d7 (diff) | |
Tacinterp: push_trace doesn't need to be wrapped in a tactic
This lets us get rid of dummy proofview manips.
Simplifications based on [(tclUNIT foo >>= f) = f foo]
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions