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/nativecode.ml | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions