diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-30 18:20:52 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-04 22:45:22 +0200 |
| commit | 7ada864b7728c9c94b7ca9856b6b2c89feb0214e (patch) | |
| tree | 0bcb36c170ae6f3c960bdc9a7bab9e3fefcc42bb /kernel/term_typing.ml | |
| parent | f6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff) | |
Fix #7631: native_compute fails to compile an example in Coq 8.8
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
Diffstat (limited to 'kernel/term_typing.ml')
0 files changed, 0 insertions, 0 deletions