From 2e75d6606220cb4b5e80766b82007f94788929fb Mon Sep 17 00:00:00 2001 From: BESSON Frederic Date: Fri, 2 Apr 2021 19:58:46 +0200 Subject: [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 --- theories/micromega/ZifyClasses.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'theories') 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. -- cgit v1.2.3