diff options
| author | Pierre-Marie Pédrot | 2019-06-09 12:19:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:38:35 +0200 |
| commit | e5c788f9efce9a9dd11910cd53c4a99451c48d8a (patch) | |
| tree | 0ef48e2c5e135bc209ffa036454dfe3c760d2046 /kernel/cbytecodes.ml | |
| parent | 3d9f2d1cbc6256c48523db00fa2cc9743a843dfe (diff) | |
Give a functional type to Ltac1 quotations with a context.
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions