We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f0b5f5b commit 191aebeCopy full SHA for 191aebe
theories/micromega/ZMicromega.v
@@ -576,7 +576,7 @@ Qed.
576
Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type) (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
577
rxcnf Zunsat Zdeduce normalise negate true f.
578
579
-#[deprecated(since="9.1", note="Use MMicromega.ZArithProof instead.")]
+(*#[deprecated(since="9.1", note="Use MMicromega.ZArithProof instead.")]*)
580
Definition ZArithProof := ZArithProof.
581
582
Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool :=
0 commit comments