diff options
| author | BESSON Frederic | 2021-04-02 19:58:46 +0200 |
|---|---|---|
| committer | Frederic Besson | 2021-04-12 10:11:32 +0200 |
| commit | 2e75d6606220cb4b5e80766b82007f94788929fb (patch) | |
| tree | 93523ccac9f241dc1519f93cfe4e60639afccda6 /tools | |
| parent | 012b8a08f142d39b2211fd52c811f830f88f2075 (diff) | |
[zify] better error reporting
The vernacular command takes a reference instead of a constr.
Moreover, the head symbol is checked i.e
Add Zify InjTyp ref checks that the referenced term has type
Intyp X1 ... Xn
Closes #14054, #13242
Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions