diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-19 16:17:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-19 16:17:40 +0200 |
| commit | c37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (patch) | |
| tree | 873e3f19156ed947e539eddcf5405e64f15e0194 /library/global.ml | |
| parent | a5722cc823dcf13594098dd21813feaaaf893bf0 (diff) | |
| parent | bc103cc493b2127f8a570bcf2e8be94378d79a55 (diff) | |
Merge PR #6754: Better elaboration of pattern-matchings on primitive projections
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions