diff options
| author | Hugo Herbelin | 2018-06-14 01:09:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-06-25 10:58:13 +0200 |
| commit | a71fdd04009aad50476d13929131713e93fcb2e2 (patch) | |
| tree | d28ee3b25ec1fdf29d818605ef88732b1e304518 /kernel/type_errors.ml | |
| parent | 915452f9a73d25e45131edb08531c29a79ab7020 (diff) | |
Critical bugs: added #3243 and Gonthier's bug in lazy machine.
Both reminded by Enrico.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions