diff options
| author | Hugo Herbelin | 2020-10-24 14:45:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-20 19:41:20 +0100 |
| commit | 93654a0ba50f26f90f84e98b33ec13caa92d1799 (patch) | |
| tree | 9ee57efbb938eeadf37e0ea80ba73bd7cb0a1722 /dev | |
| parent | 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa (diff) | |
Enforcing when a binding variable has no explicit type in constr_notation.
This avoids relying on fragile invariants.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions