diff options
| author | Pierre-Marie Pédrot | 2019-12-17 11:32:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-17 18:06:46 +0100 |
| commit | 72059138d9df96aa0c0b4be418a022167e27747e (patch) | |
| tree | 2b90aa5ea78a7ddb8ccf543c87e3eb2c7d9cc902 /dev/base_include | |
| parent | c1271dbc7763225dd1eadae8b5c8ba45b8ac5433 (diff) | |
Implementing open recursion in the pretyper.
For now, the API is unchanged and this commit only splits pretyping code for
each glob_constr constructor into a record field.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions