diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 15:58:07 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:52:14 +0200 |
| commit | 4eaafcd00992302c186b8d11e890616726ebd822 (patch) | |
| tree | 7de7b783e4721402c8e58643c62b237f4116a298 /tactics/tacsubst.ml | |
| parent | 664b3cba1e8d326382ca981aa49fdf00edd429e6 (diff) | |
Tacinterp: [interp_message] and associate now only require an environment rather than an entire goal.
Diffstat (limited to 'tactics/tacsubst.ml')
0 files changed, 0 insertions, 0 deletions