diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:38:36 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:38:36 +0200 |
| commit | d2406149554812a01ac615af43af6b7b2a3efd72 (patch) | |
| tree | 76879d5b7324f50ac482627bd4726496e70d6e24 /pretyping/pretyping.ml | |
| parent | 633b61e7ce82362a5c01724aa54b0e99dcfbb3ab (diff) | |
| parent | f18899066d7c9185cfd131cae75d076c8b2a5e01 (diff) | |
Merge PR #1046: Better error messages, fix for BZ#5723
Diffstat (limited to 'pretyping/pretyping.ml')
0 files changed, 0 insertions, 0 deletions