diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-17 08:26:01 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-17 08:26:01 +0200 |
| commit | 256ef64f9c8842ed547ee5e0521804a0c408a7f3 (patch) | |
| tree | b48c6ed367523eb70c8cbf8cf3b3e4439864bad6 /pretyping/typing.mli | |
| parent | 0651bbfa273b2adc027ddd2cfb59df2fc5ea1330 (diff) | |
| parent | b0dee52bfa97405adc7c0dbffa0f3558f349659e (diff) | |
Merge PR #7635: Define rec_declaration in terms of prec_declaration.
Diffstat (limited to 'pretyping/typing.mli')
0 files changed, 0 insertions, 0 deletions