diff options
| author | Gaëtan Gilbert | 2019-01-29 15:44:33 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-13 13:55:57 +0100 |
| commit | 454816235038540977826f1ab7ba96005639f5e1 (patch) | |
| tree | c3cd6e851a56ee83d5fafc6dca979b97c2233cbf /doc/plugin_tutorial/tuto0/src | |
| parent | 0b0fa735dc0da5660a870053a5a5f6fd1c5e22d1 (diff) | |
Fix #9432: canonical structure and coercion accept universe binders.
(when defining a new constant)
Diffstat (limited to 'doc/plugin_tutorial/tuto0/src')
0 files changed, 0 insertions, 0 deletions