diff options
| author | Hugo Herbelin | 2018-10-09 19:47:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-14 13:27:34 +0200 |
| commit | 405a80db00537b5ccfb3b8655cd7baf61e890b20 (patch) | |
| tree | 3b09bf5dc63a3ae256e4c0908ce0012a52b7ccfd /engine | |
| parent | 3a552450ddcdf96ef5b12be19ad67207697d298c (diff) | |
Passing env functionally in move_hyp and insert_decl_in_named_context.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions