diff options
| author | Hugo Herbelin | 2018-05-25 16:11:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-04 12:52:38 +0200 |
| commit | b9ad51bb8aa4fbd1bd54314797428a1a0ae19fde (patch) | |
| tree | 72b850dc2394167c248b8e629b80303fbf7cc499 /dev/include | |
| parent | 888479b3514d714253d789d9ed054eaf422f5e14 (diff) | |
Adapting to move of register_constr_interp0 from Pretyping to GlobEnv.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions