diff options
| author | Pierre-Marie Pédrot | 2014-08-19 00:52:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-19 00:58:44 +0200 |
| commit | e171b71ffa0949ca21c12d79773a6aa9b64c439e (patch) | |
| tree | 5b1bd865e6940e17bc7156c76455a6c70055c074 /pretyping/typeclasses_errors.ml | |
| parent | a398e90fe0828d62a2a2a9ecc87bd3c8d29daf8c (diff) | |
New primitive allowing to modify refine handles.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions