diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 20:16:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 20:43:16 +0100 |
| commit | edbd6a211c934778d9721c36463836ef902b4fdd (patch) | |
| tree | 0b7e03083914a80b52c862ddc0d945431d0b6d92 /pretyping/classops.mli | |
| parent | 9a6e94199b4df828f160e4a107debd7cb16e66bc (diff) | |
New bugs revealed fixed: #3408 by (probably) Maxime's commits
on vm and #3068 by Nov 2 commit on destruct.
Also fixed test for failure of #3459.
Diffstat (limited to 'pretyping/classops.mli')
0 files changed, 0 insertions, 0 deletions