diff options
| author |  Theo Zimmermann <theo.zimmermann@ens.fr> | 2015-06-19 14:53:14 +0200 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-23 15:03:08 +0200 |
| commit | 85fbcf9ed5c2f080e83f52fd2cd1791fb4172e74 (patch) | |
| tree | d9bb07f65f60d4ad68cf0059c832c8901e1aeedc /pretyping/locusops.ml | |
| parent | f3b553aa53c0dbff75bfc780209ebf33e35727fa (diff) | |
With the field record punning syntax.
Diffstat (limited to 'pretyping/locusops.ml')
0 files changed, 0 insertions, 0 deletions