aboutsummaryrefslogtreecommitdiff
path: root/theories/micromega/ZifyClasses.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/micromega/ZifyClasses.v')
-rw-r--r--theories/micromega/ZifyClasses.v11
1 files changed, 11 insertions, 0 deletions
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index f6ade67c5f..019d11d951 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.
@@ -264,3 +274,4 @@ Register impl_morph as ZifyClasses.impl_morph.
Register not as ZifyClasses.not.
Register not_morph as ZifyClasses.not_morph.
Register True as ZifyClasses.True.
+Register I as ZifyClasses.I.