diff options
| author | Vincent Laporte | 2018-11-16 11:40:49 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-11-27 09:14:43 +0000 |
| commit | b2ed1bffb7601f6bcaf3a73c110a2783451a6e26 (patch) | |
| tree | 65d86f34e6ba21becd03a2e9ba0b76b9fb7f747d /pretyping/typeclasses.ml | |
| parent | 5fcf1b7dcd9b20ea7c5ad317ce2bfe4fbb5452d9 (diff) | |
Record.declare_class: remove unused “finite” parameter
Diffstat (limited to 'pretyping/typeclasses.ml')
0 files changed, 0 insertions, 0 deletions