diff options
| author | Emilio Jesus Gallego Arias | 2020-03-23 03:43:26 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:38 -0400 |
| commit | dfcc22eeb6e5404a42d28917a5540e1d894b5a71 (patch) | |
| tree | 8d4241a530e1d0a4d3e1f8b89781cb66fb41e5ef /doc/plugin_tutorial/tuto1 | |
| parent | 7d46a32dc928af64e3e111d6d62caa00f93c427c (diff) | |
[ci] [overlays] Adapt to declare API changes.
- problem with metacoq overlay ; it expects to send a non-ground
constant to the kernel, now it fails at prepare.
Record Sigma (A : Type) (B : A -> Type) : Type :=
{ fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.
Quote Recursively Definition foo := (fst, snd).
There is a hack on the overlay, we need to discuss it a bit more.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions