diff options
| author | Pierre-Marie Pédrot | 2014-08-21 14:59:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-21 15:20:52 +0200 |
| commit | 1fbcea38dc9d995f7c6786b543675ba27970642e (patch) | |
| tree | c1d574f081038b403313daaed905521a5964603c /pretyping/typeclasses_errors.mli | |
| parent | 9a24bc736d5782b7b9c23ebd4cfcf5f5f99836eb (diff) | |
Removing unused parts of the Goal.sensitive monad.
Some legacy code remains to keep the newish refine tactic working, but
ultimately it should be removed. I did not manage to do it properly though,
i.e. without breaking the test-suite furthermore.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions