diff options
| author | Pierre-Marie Pédrot | 2013-11-26 21:17:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-26 21:22:20 +0100 |
| commit | e057d9cb8276d1d727825a940673bfb95660ddf5 (patch) | |
| tree | 04229e6c8a7d0f3b9e9b7cda4aa4697f2eb8dad0 /kernel | |
| parent | 51d4da4ac126b4b3bb033ec88253866345594e01 (diff) | |
Do not use ugly Dyn features in the Quote plugin. Use instead the
provided tactic environment to handle open terms.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions