diff options
| author | Pierre-Marie Pédrot | 2014-08-19 01:06:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-19 01:07:31 +0200 |
| commit | 56ece74efc25af1b0e09265f3c7fcf74323abcaf (patch) | |
| tree | 56d854b6484ffc8525b4203b57a1d344e91b9940 /pretyping/typeclasses_errors.ml | |
| parent | e171b71ffa0949ca21c12d79773a6aa9b64c439e (diff) | |
Removing a use of Goal.refine.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions