File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change 576
576
Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type ) (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
577
577
rxcnf Zunsat Zdeduce normalise negate true f.
578
578
579
- (* #[deprecated(since="9.1 ", note="Use MMicromega.ZArithProof instead.")] *)
579
+ #[deprecated(since="9.0 ", note="Use MMicromega.ZArithProof instead.")]
580
580
Definition ZArithProof := ZArithProof.
581
581
582
582
Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool :=
Original file line number Diff line number Diff line change 1
- Attributes deprecated(since="9.1 ", note="Use TifyClasses instead.").
1
+ Attributes deprecated(since="9.0 ", note="Use TifyClasses instead.").
2
2
3
3
From Stdlib Require Export TifyClasses.
4
4
You can’t perform that action at this time.
0 commit comments