diff options
| author | Pierre-Marie Pédrot | 2014-01-14 09:03:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-14 09:03:44 +0100 |
| commit | b8d31eb7f359dd842c1b53b1b74725158fc01c1e (patch) | |
| tree | 496463f667544a45565ae549ddba4a2b77c6a1ee /kernel/type_errors.ml | |
| parent | 679132dd7b193c5d19066696871ca13fafc35654 (diff) | |
Removing unused tactics in rewrite.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions