diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 10:09:53 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 10:09:53 +0100 |
commit | db8fcbb7763ac784f7c72b72509d5dc7c2c5323c (patch) | |
tree | 44b43bcbdec48ac23a458e2c525e9a716592b4aa /vernac/auto_ind_decl.ml | |
parent | ddc9728030a98b03447e321d2eb4af0d92add11f (diff) | |
parent | 50c948480647af3c5aaea5f80fa9f3341471f2b0 (diff) |
Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of a record.
Diffstat (limited to 'vernac/auto_ind_decl.ml')
0 files changed, 0 insertions, 0 deletions