diff options
| author | Pierre-Marie Pédrot | 2016-05-16 21:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 22:16:36 +0200 |
| commit | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (patch) | |
| tree | dd9e7016271fdad02452aed0f8cd469305e0780e /kernel/type_errors.mli | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions