diff options
| author | Vincent Laporte | 2021-04-12 15:27:31 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2021-04-12 15:27:31 +0200 |
| commit | bc49ee6872f1a5bb781c8b81bc21371d93492841 (patch) | |
| tree | 87b5fbefca4199d3d06f4cbaaee907128ec702a1 /theories | |
| parent | 271445decd0fc1a37da3009f148f2e68c7168fe1 (diff) | |
| parent | 2e75d6606220cb4b5e80766b82007f94788929fb (diff) | |
Merge PR #14061: [zify] better error reporting
Reviewed-by: vbgl
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. |