diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-11 18:18:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-11 19:38:24 +0200 |
| commit | 2a2d418971a019202cdb78fabc7658a543f0886d (patch) | |
| tree | 0292c97712ab9ac39b1595a498aec131cbc1227f /plugins/extraction/extract_env.ml | |
| parent | 7bc1610376fac29397be39d4a06b178e8e35e66e (diff) | |
Adding a test to check whether two tactic notations conflict.
Diffstat (limited to 'plugins/extraction/extract_env.ml')
0 files changed, 0 insertions, 0 deletions