diff options
| author | Pierre-Marie Pédrot | 2014-08-15 14:03:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-15 14:07:13 +0200 |
| commit | aae3c3b42a9bad20ebde4a139e6de660fbb8e042 (patch) | |
| tree | 188895bdaa3835f6175406fb0d22e282441448a5 /pretyping/typeclasses_errors.ml | |
| parent | c69404402212ed9d541899ae78ac889e62cf238a (diff) | |
Removing unused Refiner.tclWITHHOLES.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions