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 /theories | |
| 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 'theories')
| -rw-r--r-- | theories/micromega/ZifyClasses.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index f6ade67c5f..a08a56b20e 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -250,8 +250,18 @@ Register rew_iff as ZifyClasses.rew_iff. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. + +Register InjTyp as ZifyClasses.InjTyp. +Register BinOp as ZifyClasses.BinOp. +Register UnOp as ZifyClasses.UnOp. +Register CstOp as ZifyClasses.CstOp. +Register BinRel as ZifyClasses.BinRel. +Register PropOp as ZifyClasses.PropOp. +Register PropUOp as ZifyClasses.PropUOp. Register BinOpSpec as ZifyClasses.BinOpSpec. Register UnOpSpec as ZifyClasses.UnOpSpec. +Register Saturate as ZifyClasses.Saturate. + (** Propositional logic *) Register and as ZifyClasses.and. |