diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-31 12:53:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-31 15:09:49 +0200 |
| commit | 20c2176e8b0b64737fad8dbc1fbc9ef2d182372d (patch) | |
| tree | 6bbcc249dd6115ccd32a3e788c548cc5cdb6e1dd /interp | |
| parent | 29bb2f7d9fecf06e3246142e649db4db0320da41 (diff) | |
Getting rid of atomic tactics in Tacenv.
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions