[fix] for backward compat

Author: fajb

theories/micromega/ZMicromega.v

@@ -576,6 +576,9 @@ Qed.
 Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type)  (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
   rxcnf Zunsat Zdeduce normalise negate true f.
 
+#[deprecated(since="9.1", note="Use MMicromega.ZArithProof instead.")]
+Definition ZArithProof := ZArithProof.
+
 Definition ZTautoChecker  (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool :=
   @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate  ZArithProof (fun cl => ZChecker None (List.map fst cl)) f w.
 

theories/micromega/ZifyInst.v

@@ -14,6 +14,7 @@
 
 From Stdlib Require Import Arith BinInt BinNat Zeven Znat Nnat.
 From Stdlib Require Import TifyClasses.
+From Stdlib Require Import ZifyClasses. (* for backward compatibility - to be removed *)
 Declare ML Module "rocq-runtime.plugins.zify".
 Local Open Scope Z_scope.