diff options
| author | Pierre-Marie Pédrot | 2014-10-12 16:51:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-10-12 16:51:05 +0200 |
| commit | 7e8b7bc5fd911d2fb34eecd238788fc2e81afa0f (patch) | |
| tree | 36514b1191af95910430386b7a082af2d7642b6f /kernel/modops.mli | |
| parent | d4b3de96f524887013c0955bd5b90f0311f086e6 (diff) | |
Tentative fix for a badly used Option.get in Reductionops.
Diffstat (limited to 'kernel/modops.mli')
0 files changed, 0 insertions, 0 deletions