Update zify documentation

Add Zify <X> are documented.
Add <X> is deprecated as it clashed with the standard Add command

6 files changed, 212 insertions, 170 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 717b0deb43..c4947e6b3a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -284,37 +284,54 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
    + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``.
 
+   The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
+   The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
 
-.. cmd:: Show Zify InjTyp
-   :name: Show Zify InjTyp
+.. cmd:: Add Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec } @qualid
 
-   This command shows the list of types that can be injected into :g:`Z`.
+   This command registers an instance of one of the typeclasses among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``,  ``BinRel``,
+   ``UnOpSpec``, ``BinOpSpec``.
 
-.. cmd:: Show Zify BinOp
-   :name: Show Zify BinOp
+.. cmd:: Show Zify {| InjTyp | BinOp | UnOp |CstOp | BinRel | UnOpSpec | BinOpSpec }
 
-   This command shows the list of binary operators processed by :tacn:`zify`.
+   The command prints the typeclass instances of one the typeclasses
+   among ``InjTyp``, ``BinOp``, ``UnOp``, ``CstOp``, ``BinRel``,
+   ``UnOpSpec``, ``BinOpSpec``. For instance, :cmd:`Show Zify` ``InjTyp``
+   prints the list of types that supported by :tacn:`zify` i.e.,
+   :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
-.. cmd:: Show Zify BinRel
-   :name: Show Zify BinRel
+.. cmd:: Show Zify Spec
 
-   This command shows the list of binary relations processed by :tacn:`zify`.
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec``.
 
+.. cmd:: Add InjTyp
 
-.. cmd:: Show Zify UnOp
-   :name: Show Zify UnOp
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``InjTyp``.
 
-   This command shows the list of unary operators processed by :tacn:`zify`.
+.. cmd:: Add BinOp
 
-.. cmd:: Show Zify CstOp
-   :name: Show Zify CstOp
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``BinOp``.
+
+.. cmd:: Add UnOp
+
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``UnOp``.
+
+.. cmd:: Add CstOp
+
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``CstOp``.
+
+.. cmd:: Add BinRel
+
+   .. deprecated:: 8.13
+       Use instead either :cmd:`Add Zify` ``BinRel``.
 
-   This command shows the list of constants processed by :tacn:`zify`.
 
-.. cmd:: Show Zify Spec
-   :name: Show Zify Spec
 
-   This command shows the list of operators over :g:`Z` that are compiled using their specification e.g., :g:`Z.min`.
 
 .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#fnpsatz] Variants deal with equalities and strict inequalities.
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 80a40c4315..0e5cac2d4a 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -14,23 +14,44 @@ open Ltac_plugin
 open Stdarg
 open Tacarg
 
+let warn_deprecated_Spec =
+  CWarnings.create ~name:"deprecated-Zify-Spec" ~category:"deprecated"
+    (fun () ->
+      Pp.strbrk ("Show Zify Spec is deprecated. Use either \"Show Zify BinOpSpec\" or \"Show Zify UnOpSpec\"."))
+
+let warn_deprecated_Add =
+  CWarnings.create ~name:"deprecated-Zify-Add" ~category:"deprecated"
+    (fun () ->
+      Pp.strbrk ("Add <X> is deprecated. Use instead Add Zify <X>."))
+
 
 }
 
 DECLARE PLUGIN "zify_plugin"
 
 VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
-| ["Add" "InjTyp"    constr(t) ] -> { Zify.InjTable.register t }
-| ["Add" "BinOp"     constr(t) ] -> { Zify.BinOp.register t }
-| ["Add" "UnOp"      constr(t) ] -> { Zify.UnOp.register t }
-| ["Add" "CstOp"     constr(t) ] -> { Zify.CstOp.register t }
-| ["Add" "BinRel"    constr(t) ] -> { Zify.BinRel.register t }
-| ["Add" "PropOp"    constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "PropBinOp"    constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "PropUOp"   constr(t) ] -> { Zify.PropUnOp.register t }
-| ["Add" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
-| ["Add" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
-| ["Add" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
+| ["Add" "Zify" "InjTyp"    constr(t) ] -> { Zify.InjTable.register t }
+| ["Add" "Zify" "BinOp"     constr(t) ] -> { Zify.BinOp.register t }
+| ["Add" "Zify" "UnOp"      constr(t) ] -> { Zify.UnOp.register t }
+| ["Add" "Zify" "CstOp"     constr(t) ] -> { Zify.CstOp.register t }
+| ["Add" "Zify" "BinRel"    constr(t) ] -> { Zify.BinRel.register t }
+| ["Add" "Zify" "PropOp"    constr(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropBinOp"    constr(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropUOp"   constr(t) ] -> { Zify.PropUnOp.register t }
+| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
+| ["Add" "Zify" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
+| ["Add" "Zify" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
+| ["Add" "InjTyp"    constr(t) ] -> { warn_deprecated_Add (); Zify.InjTable.register t }
+| ["Add" "BinOp"     constr(t) ] -> { warn_deprecated_Add (); Zify.BinOp.register t }
+| ["Add" "UnOp"      constr(t) ] -> { warn_deprecated_Add (); Zify.UnOp.register t }
+| ["Add" "CstOp"     constr(t) ] -> { warn_deprecated_Add (); Zify.CstOp.register t }
+| ["Add" "BinRel"    constr(t) ] -> { warn_deprecated_Add (); Zify.BinRel.register t }
+| ["Add" "PropOp"    constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t }
+| ["Add" "PropBinOp"    constr(t) ] -> { warn_deprecated_Add (); Zify.PropBinOp.register t }
+| ["Add" "PropUOp"   constr(t) ] -> { warn_deprecated_Add (); Zify.PropUnOp.register t }
+| ["Add" "BinOpSpec" constr(t) ] -> { warn_deprecated_Add (); Zify.BinOpSpec.register t }
+| ["Add" "UnOpSpec"  constr(t) ] -> { warn_deprecated_Add (); Zify.UnOpSpec.register t }
+| ["Add" "Saturate"  constr(t) ] -> { warn_deprecated_Add (); Zify.Saturate.register t }
 END
 
 TACTIC EXTEND ITER
@@ -50,6 +71,9 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
 |[ "Show" "Zify" "UnOp" ]   -> { Zify.UnOp.print () }
 |[ "Show" "Zify" "CstOp"]   -> { Zify.CstOp.print () }
 |[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
-|[ "Show" "Zify" "Spec"] -> { (* This prints both UnOpSpec and BinOpSpec *)
-    Zify.UnOpSpec.print() }
+|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() }
+|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() }
+|[ "Show" "Zify" "Spec"] -> {
+    warn_deprecated_Spec () ;
+    Zify.UnOpSpec.print() ; Zify.BinOpSpec.print ()}
 END
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index ec0f278326..4e1f9a66ac 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -320,7 +320,8 @@ type decl_kind =
   | UnOp of EUnOpT.t decl
   | CstOp of ECstOpT.t decl
   | Saturate of ESatT.t decl
-  | Spec of ESpecT.t decl
+  | UnOpSpec of ESpecT.t decl
+  | BinOpSpec of ESpecT.t decl
 
 type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr
 
@@ -664,8 +665,8 @@ module EUnopSpec = struct
 
   let name = "UnopSpec"
   let table = specs
-  let cast x = Spec x
-  let dest = function Spec x -> Some x | _ -> None
+  let cast x = UnOpSpec x
+  let dest = function UnOpSpec x -> Some x | _ -> None
   let mk_elt evd i a = {spec = a.(4)}
   let get_key = 2
 end
@@ -677,8 +678,8 @@ module EBinOpSpec = struct
 
   let name = "BinOpSpec"
   let table = specs
-  let cast x = Spec x
-  let dest = function Spec x -> Some x | _ -> None
+  let cast x = BinOpSpec x
+  let dest = function BinOpSpec x -> Some x | _ -> None
   let mk_elt evd i a = {spec = a.(5)}
   let get_key = 3
 end
@@ -1419,7 +1420,7 @@ let rec spec_of_term env evd (senv : spec_env) t =
     with Not_found -> (
       try
         match snd (HConstr.find c !specs_cache) with
-        | Spec s ->
+        | UnOpSpec s | BinOpSpec s ->
           let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in
           register_constr senv' t' thm
         | _ -> (get_name t' senv', senv')
diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v
index 6c34040155..fa3f123b18 100644
--- a/theories/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
@@ -16,21 +16,21 @@ Local Open Scope Z_scope.
 Instance Inj_bool_bool : InjTyp bool bool :=
   { inj := (fun x => x) ; pred := (fun b => b = true \/ b = false) ;
     cstr := (ltac:(intro b; destruct b; tauto))}.
-Add InjTyp Inj_bool_bool.
+Add Zify InjTyp Inj_bool_bool.
 
 (** Boolean operators *)
 
 Instance Op_andb : BinOp andb :=
   { TBOp := andb ; TBOpInj := fun _ _  => eq_refl}.
-Add BinOp Op_andb.
+Add Zify BinOp Op_andb.
 
 Instance Op_orb : BinOp orb :=
   { TBOp := orb ; TBOpInj := fun _ _ => eq_refl}.
-Add BinOp Op_orb.
+Add Zify BinOp Op_orb.
 
 Instance Op_implb : BinOp implb :=
   { TBOp := implb; TBOpInj := fun _ _ => eq_refl }.
-Add BinOp Op_implb.
+Add Zify BinOp Op_implb.
 
 Definition xorb_eq : forall b1 b2,
     xorb b1 b2 = andb (orb b1 b2) (negb (eqb b1 b2)).
@@ -40,49 +40,49 @@ Qed.
 
 Instance Op_xorb : BinOp xorb :=
   { TBOp := fun x y => andb (orb x y) (negb (eqb x y)); TBOpInj := xorb_eq }.
-Add BinOp Op_xorb.
+Add Zify BinOp Op_xorb.
 
 Instance Op_eqb : BinOp eqb :=
   { TBOp := eqb; TBOpInj := fun _ _ => eq_refl }.
-Add BinOp Op_eqb.
+Add Zify BinOp Op_eqb.
 
 Instance Op_negb : UnOp negb :=
   { TUOp := negb ; TUOpInj := fun _ => eq_refl}.
-Add UnOp Op_negb.
+Add Zify UnOp Op_negb.
 
 Instance Op_eq_bool : BinRel (@eq bool) :=
   {TR := @eq bool ; TRInj := ltac:(reflexivity) }.
-Add BinRel Op_eq_bool.
+Add Zify BinRel Op_eq_bool.
 
 Instance Op_true : CstOp true :=
   { TCst := true ; TCstInj := eq_refl }.
-Add CstOp Op_true.
+Add Zify CstOp Op_true.
 
 Instance Op_false : CstOp false :=
   { TCst := false ; TCstInj := eq_refl }.
-Add CstOp Op_false.
+Add Zify CstOp Op_false.
 
 (** Comparison over Z *)
 
 Instance Op_Zeqb : BinOp Z.eqb :=
   { TBOp := Z.eqb ; TBOpInj := fun _ _ => eq_refl }.
-Add BinOp Op_Zeqb.
+Add Zify BinOp Op_Zeqb.
 
 Instance Op_Zleb : BinOp Z.leb :=
   { TBOp := Z.leb; TBOpInj :=  fun _ _ => eq_refl }.
-Add BinOp Op_Zleb.
+Add Zify BinOp Op_Zleb.
 
 Instance Op_Zgeb : BinOp Z.geb :=
   { TBOp := Z.geb; TBOpInj := fun _ _ => eq_refl }.
-Add BinOp Op_Zgeb.
+Add Zify BinOp Op_Zgeb.
 
 Instance Op_Zltb : BinOp Z.ltb :=
   { TBOp := Z.ltb ; TBOpInj := fun _ _ => eq_refl }.
-Add BinOp Op_Zltb.
+Add Zify BinOp Op_Zltb.
 
 Instance Op_Zgtb : BinOp Z.gtb :=
   { TBOp := Z.gtb; TBOpInj := fun _ _  => eq_refl }.
-Add BinOp Op_Zgtb.
+Add Zify BinOp Op_Zgtb.
 
 (** Comparison over nat *)
 
@@ -118,15 +118,15 @@ Qed.
 
 Instance Op_nat_eqb : BinOp Nat.eqb :=
   { TBOp := Z.eqb; TBOpInj := Z_of_nat_eqb_iff }.
-Add BinOp Op_nat_eqb.
+Add Zify BinOp Op_nat_eqb.
 
 Instance Op_nat_leb : BinOp Nat.leb :=
   { TBOp := Z.leb; TBOpInj := Z_of_nat_leb_iff }.
-Add BinOp Op_nat_leb.
+Add Zify BinOp Op_nat_leb.
 
 Instance Op_nat_ltb : BinOp Nat.ltb :=
   { TBOp := Z.ltb; TBOpInj := Z_of_nat_ltb_iff }.
-Add BinOp Op_nat_ltb.
+Add Zify BinOp Op_nat_ltb.
 
 Lemma b2n_b2z :  forall x,  Z.of_nat (Nat.b2n x) = Z.b2z x.
 Proof.
@@ -135,11 +135,11 @@ Qed.
 
 Instance Op_b2n : UnOp Nat.b2n :=
   { TUOp := Z.b2z; TUOpInj := b2n_b2z }.
-Add UnOp Op_b2n.
+Add Zify UnOp Op_b2n.
 
 Instance Op_b2z : UnOp Z.b2z :=
   { TUOp := Z.b2z; TUOpInj := fun _ => eq_refl }.
-Add UnOp Op_b2z.
+Add Zify UnOp Op_b2z.
 
 Lemma b2z_spec : forall b, (b = true /\ Z.b2z b = 1) \/ (b = false /\ Z.b2z b = 0).
 Proof.
@@ -150,7 +150,7 @@ Instance b2zSpec : UnOpSpec Z.b2z :=
   { UPred := fun b r => (b = true /\ r = 1) \/ (b = false /\ r = 0);
     USpec := b2z_spec
   }.
-Add UnOpSpec b2zSpec.
+Add Zify UnOpSpec b2zSpec.
 
 Ltac elim_bool_cstr :=
   repeat match goal with
diff --git a/theories/micromega/ZifyComparison.v b/theories/micromega/ZifyComparison.v
index b8d38adcc5..a4ada571f1 100644
--- a/theories/micromega/ZifyComparison.v
+++ b/theories/micromega/ZifyComparison.v
@@ -28,30 +28,30 @@ Qed.
 
 Instance Inj_comparison_Z : InjTyp comparison Z :=
   { inj := Z_of_comparison ; pred :=(fun x => -1 <= x <= 1) ; cstr := Z_of_comparison_bound}.
-Add InjTyp Inj_comparison_Z.
+Add Zify InjTyp Inj_comparison_Z.
 
 Definition ZcompareZ (x y : Z) :=
   Z_of_comparison (Z.compare x y).
 
 Program Instance BinOp_Zcompare : BinOp Z.compare :=
   { TBOp := ZcompareZ }.
-Add BinOp BinOp_Zcompare.
+Add Zify BinOp BinOp_Zcompare.
 
 Instance Op_eq_comparison : BinRel (@eq comparison) :=
   {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.
-Add BinRel Op_eq_comparison.
+Add Zify BinRel Op_eq_comparison.
 
 Instance Op_Eq : CstOp Eq :=
   { TCst := 0 ; TCstInj := eq_refl }.
-Add CstOp Op_Eq.
+Add Zify CstOp Op_Eq.
 
 Instance Op_Lt : CstOp Lt :=
   { TCst := -1 ; TCstInj := eq_refl }.
-Add CstOp Op_Lt.
+Add Zify CstOp Op_Lt.
 
 Instance Op_Gt : CstOp Gt :=
   { TCst := 1 ; TCstInj := eq_refl }.
-Add CstOp Op_Gt.
+Add Zify CstOp Op_Gt.
 
 
 Lemma Zcompare_spec : forall x y,
@@ -79,4 +79,4 @@ Instance ZcompareSpec : BinOpSpec ZcompareZ :=
                            /\
                            (x < y  -> r = -1)
               ; BSpec := Zcompare_spec|}.
-Add BinOpSpec ZcompareSpec.
+Add Zify BinOpSpec ZcompareSpec.
diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index e5d0312f3d..0e135ba793 100644
--- a/theories/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
@@ -25,117 +25,117 @@ Ltac refl :=
 
 Instance Inj_Z_Z : InjTyp Z Z :=
   mkinj _ _ (fun x => x) (fun x =>  True ) (fun _ => I).
-Add InjTyp Inj_Z_Z.
+Add Zify InjTyp Inj_Z_Z.
 
 (** Support for nat *)
 
 Instance Inj_nat_Z : InjTyp nat Z :=
   mkinj _ _ Z.of_nat (fun x =>  0 <= x ) Nat2Z.is_nonneg.
-Add InjTyp Inj_nat_Z.
+Add Zify InjTyp Inj_nat_Z.
 
 (* zify_nat_rel *)
 Instance Op_ge : BinRel ge :=
   {| TR := Z.ge; TRInj := Nat2Z.inj_ge |}.
-Add BinRel Op_ge.
+Add Zify BinRel Op_ge.
 
 Instance Op_lt : BinRel lt :=
   {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}.
-Add BinRel Op_lt.
+Add Zify BinRel Op_lt.
 
 Instance Op_Nat_lt : BinRel Nat.lt := Op_lt.
-Add BinRel Op_Nat_lt.
+Add Zify BinRel Op_Nat_lt.
 
 Instance Op_gt : BinRel gt :=
   {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}.
-Add BinRel Op_gt.
+Add Zify BinRel Op_gt.
 
 Instance Op_le : BinRel le :=
   {| TR := Z.le; TRInj := Nat2Z.inj_le |}.
-Add BinRel Op_le.
+Add Zify BinRel Op_le.
 
 Instance Op_Nat_le : BinRel Nat.le := Op_le.
-Add BinRel Op_Nat_le.
+Add Zify BinRel Op_Nat_le.
 
 Instance Op_eq_nat : BinRel (@eq nat) :=
   {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}.
-Add BinRel Op_eq_nat.
+Add Zify BinRel Op_eq_nat.
 
 Instance Op_Nat_eq : BinRel (Nat.eq) := Op_eq_nat.
-Add BinRel Op_Nat_eq.
+Add Zify BinRel Op_Nat_eq.
 
 (* zify_nat_op *)
 Instance Op_plus : BinOp Nat.add :=
   {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}.
-Add BinOp Op_plus.
+Add Zify BinOp Op_plus.
 
 Instance Op_sub : BinOp Nat.sub :=
   {| TBOp := fun n m => Z.max 0 (n - m) ; TBOpInj := Nat2Z.inj_sub_max |}.
-Add BinOp Op_sub.
+Add Zify BinOp Op_sub.
 
 Instance Op_mul : BinOp Nat.mul :=
   {| TBOp := Z.mul ; TBOpInj := Nat2Z.inj_mul |}.
-Add BinOp Op_mul.
+Add Zify BinOp Op_mul.
 
 Instance Op_min : BinOp Nat.min :=
   {| TBOp := Z.min ; TBOpInj := Nat2Z.inj_min |}.
-Add BinOp Op_min.
+Add Zify BinOp Op_min.
 
 Instance Op_max : BinOp Nat.max :=
   {| TBOp := Z.max ; TBOpInj := Nat2Z.inj_max |}.
-Add BinOp Op_max.
+Add Zify BinOp Op_max.
 
 Instance Op_pred : UnOp Nat.pred :=
   {| TUOp := fun n => Z.max 0 (n - 1) ; TUOpInj := Nat2Z.inj_pred_max |}.
-Add UnOp Op_pred.
+Add Zify UnOp Op_pred.
 
 Instance Op_S : UnOp S :=
   {| TUOp := fun x => Z.add x 1 ; TUOpInj := Nat2Z.inj_succ |}.
-Add UnOp Op_S.
+Add Zify UnOp Op_S.
 
 Instance Op_O : CstOp O :=
   {| TCst := Z0 ; TCstInj := eq_refl (Z.of_nat 0) |}.
-Add CstOp Op_O.
+Add Zify CstOp Op_O.
 
 Instance Op_Z_abs_nat : UnOp  Z.abs_nat :=
   { TUOp := Z.abs ; TUOpInj := Zabs2Nat.id_abs }.
-Add UnOp Op_Z_abs_nat.
+Add Zify UnOp Op_Z_abs_nat.
 
 (** Support for positive *)
 
 Instance Inj_pos_Z : InjTyp positive Z :=
   {| inj := Zpos ; pred := (fun x =>  0 < x ) ; cstr := Pos2Z.pos_is_pos |}.
-Add InjTyp Inj_pos_Z.
+Add Zify InjTyp Inj_pos_Z.
 
 Instance Op_pos_to_nat : UnOp  Pos.to_nat :=
   {TUOp := (fun x => x); TUOpInj := positive_nat_Z}.
-Add UnOp Op_pos_to_nat.
+Add Zify UnOp Op_pos_to_nat.
 
 Instance Inj_N_Z : InjTyp N Z :=
   mkinj _ _ Z.of_N (fun x =>  0 <= x ) N2Z.is_nonneg.
-Add InjTyp Inj_N_Z.
+Add Zify InjTyp Inj_N_Z.
 
 
 Instance Op_N_to_nat : UnOp  N.to_nat :=
   { TUOp := fun x => x ; TUOpInj := N_nat_Z }.
-Add UnOp Op_N_to_nat.
+Add Zify UnOp Op_N_to_nat.
 
 (* zify_positive_rel *)
 
 Instance Op_pos_ge : BinRel Pos.ge :=
   {| TR := Z.ge; TRInj := fun x y => iff_refl (Z.pos x >= Z.pos y) |}.
-Add BinRel Op_pos_ge.
+Add Zify BinRel Op_pos_ge.
 
 Instance Op_pos_lt : BinRel Pos.lt :=
   {| TR := Z.lt; TRInj := fun x y => iff_refl (Z.pos x < Z.pos y) |}.
-Add BinRel Op_pos_lt.
+Add Zify BinRel Op_pos_lt.
 
 Instance Op_pos_gt : BinRel Pos.gt :=
   {| TR := Z.gt; TRInj := fun x y => iff_refl (Z.pos x > Z.pos y)  |}.
-Add BinRel Op_pos_gt.
+Add Zify BinRel Op_pos_gt.
 
 Instance Op_pos_le : BinRel Pos.le :=
   {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}.
-Add BinRel Op_pos_le.
+Add Zify BinRel Op_pos_le.
 
 Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y.
 Proof.
@@ -145,36 +145,36 @@ Qed.
 
 Instance Op_eq_pos : BinRel (@eq positive) :=
   { TR := @eq Z ; TRInj := eq_pos_inj }.
-Add BinRel Op_eq_pos.
+Add Zify BinRel Op_eq_pos.
 
 (* zify_positive_op *)
 
 Instance Op_Z_of_N : UnOp Z.of_N :=
   { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }.
-Add UnOp Op_Z_of_N.
+Add Zify UnOp Op_Z_of_N.
 
 Instance Op_Z_to_N : UnOp Z.to_N :=
   { TUOp := fun x => Z.max 0 x ; TUOpInj := ltac:(now intro x; destruct x) }.
-Add UnOp Op_Z_to_N.
+Add Zify UnOp Op_Z_to_N.
 
 Instance Op_Z_neg : UnOp Z.neg :=
   { TUOp :=  Z.opp ; TUOpInj := (fun x => eq_refl (Zneg x))}.
-Add UnOp Op_Z_neg.
+Add Zify UnOp Op_Z_neg.
 
 Instance Op_Z_pos : UnOp Z.pos :=
   { TUOp := (fun x =>  x) ; TUOpInj := (fun x => eq_refl (Z.pos x))}.
-Add UnOp Op_Z_pos.
+Add Zify UnOp Op_Z_pos.
 
 Instance Op_pos_succ : UnOp Pos.succ :=
   { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ  }.
-Add UnOp Op_pos_succ.
+Add Zify UnOp Op_pos_succ.
 
 
 
 
 Instance Op_pos_pred_double : UnOp Pos.pred_double :=
 { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(refl) }.
-Add UnOp Op_pos_pred_double.
+Add Zify UnOp Op_pos_pred_double.
 
 Instance Op_pos_pred : UnOp Pos.pred :=
   { TUOp := fun x => Z.max 1 (x - 1) ;
@@ -182,266 +182,266 @@ Instance Op_pos_pred : UnOp Pos.pred :=
                  (intros;
                     rewrite <- Pos.sub_1_r;
                     apply Pos2Z.inj_sub_max) }.
-Add UnOp Op_pos_pred.
+Add Zify UnOp Op_pos_pred.
 
 Instance Op_pos_predN : UnOp Pos.pred_N :=
   { TUOp := fun x => x - 1 ;
     TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }.
-Add UnOp Op_pos_predN.
+Add Zify UnOp Op_pos_predN.
 
 Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat :=
   { TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }.
-Add UnOp Op_pos_of_succ_nat.
+Add Zify UnOp Op_pos_of_succ_nat.
 
 Instance Op_pos_of_nat : UnOp Pos.of_nat :=
   { TUOp := fun x => Z.max 1 x ;
     TUOpInj := ltac: (now destruct x;
                         [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }.
-Add UnOp Op_pos_of_nat.
+Add Zify UnOp Op_pos_of_nat.
 
 Instance Op_pos_add : BinOp Pos.add :=
   { TBOp := Z.add ; TBOpInj := ltac: (refl) }.
-Add BinOp Op_pos_add.
+Add Zify BinOp Op_pos_add.
 
 Instance Op_pos_add_carry : BinOp Pos.add_carry :=
   { TBOp := fun x y => x + y + 1 ;
     TBOpInj := ltac:(now intros; rewrite Pos.add_carry_spec, Pos2Z.inj_succ) }.
-Add BinOp Op_pos_add_carry.
+Add Zify BinOp Op_pos_add_carry.
 
 Instance Op_pos_sub : BinOp Pos.sub :=
   { TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }.
-Add BinOp Op_pos_sub.
+Add Zify BinOp Op_pos_sub.
 
 Instance Op_pos_mul : BinOp Pos.mul :=
   { TBOp :=  Z.mul ; TBOpInj := ltac: (refl) }.
-Add BinOp Op_pos_mul.
+Add Zify BinOp Op_pos_mul.
 
 Instance Op_pos_min : BinOp Pos.min :=
   { TBOp := Z.min ; TBOpInj := Pos2Z.inj_min }.
-Add BinOp Op_pos_min.
+Add Zify BinOp Op_pos_min.
 
 Instance Op_pos_max : BinOp Pos.max :=
   { TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }.
-Add BinOp Op_pos_max.
+Add Zify BinOp Op_pos_max.
 
 Instance Op_pos_pow : BinOp Pos.pow :=
   { TBOp := Z.pow ; TBOpInj := Pos2Z.inj_pow }.
-Add BinOp Op_pos_pow.
+Add Zify BinOp Op_pos_pow.
 
 Instance Op_pos_square : UnOp Pos.square :=
   { TUOp := Z.square ; TUOpInj := Pos2Z.inj_square }.
-Add UnOp Op_pos_square.
+Add Zify UnOp Op_pos_square.
 
 Instance Op_xO : UnOp xO :=
   { TUOp := fun x => 2 * x ; TUOpInj := ltac: (refl) }.
-Add UnOp Op_xO.
+Add Zify UnOp Op_xO.
 
 Instance Op_xI : UnOp xI :=
   { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (refl) }.
-Add UnOp Op_xI.
+Add Zify UnOp Op_xI.
 
 Instance Op_xH : CstOp xH :=
   { TCst := 1%Z ; TCstInj := ltac:(refl)}.
-Add CstOp Op_xH.
+Add Zify CstOp Op_xH.
 
 Instance Op_Z_of_nat : UnOp Z.of_nat:=
   { TUOp := fun x => x ; TUOpInj := (fun x : nat => @eq_refl Z (Z.of_nat x)) }.
-Add UnOp Op_Z_of_nat.
+Add Zify UnOp Op_Z_of_nat.
 
 (* zify_N_rel *)
 Instance Op_N_ge : BinRel N.ge :=
   {| TR := Z.ge ; TRInj := N2Z.inj_ge |}.
-Add BinRel Op_N_ge.
+Add Zify BinRel Op_N_ge.
 
 Instance Op_N_lt : BinRel N.lt :=
   {| TR := Z.lt ; TRInj := N2Z.inj_lt |}.
-Add BinRel Op_N_lt.
+Add Zify BinRel Op_N_lt.
 
 Instance Op_N_gt : BinRel N.gt :=
   {| TR := Z.gt ; TRInj := N2Z.inj_gt |}.
-Add BinRel Op_N_gt.
+Add Zify BinRel Op_N_gt.
 
 Instance Op_N_le : BinRel N.le :=
   {| TR := Z.le ; TRInj := N2Z.inj_le |}.
-Add BinRel Op_N_le.
+Add Zify BinRel Op_N_le.
 
 Instance Op_eq_N : BinRel (@eq N) :=
   {| TR := @eq Z ; TRInj := fun x y : N => iff_sym (N2Z.inj_iff x y) |}.
-Add BinRel Op_eq_N.
+Add Zify BinRel Op_eq_N.
 
 (* zify_N_op *)
 Instance Op_N_N0 : CstOp  N0 :=
   { TCst := Z0 ; TCstInj := eq_refl }.
-Add CstOp Op_N_N0.
+Add Zify CstOp Op_N_N0.
 
 Instance Op_N_Npos : UnOp  Npos :=
   { TUOp := (fun x => x) ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_N_Npos.
+Add Zify UnOp Op_N_Npos.
 
 Instance Op_N_of_nat : UnOp  N.of_nat :=
   { TUOp := fun x => x ; TUOpInj := nat_N_Z }.
-Add UnOp Op_N_of_nat.
+Add Zify UnOp Op_N_of_nat.
 
 Instance Op_Z_abs_N : UnOp Z.abs_N :=
   { TUOp := Z.abs ; TUOpInj := N2Z.inj_abs_N }.
-Add UnOp Op_Z_abs_N.
+Add Zify UnOp Op_Z_abs_N.
 
 Instance Op_N_pos : UnOp N.pos :=
   { TUOp := fun x => x ; TUOpInj := ltac:(refl)}.
-Add UnOp Op_N_pos.
+Add Zify UnOp Op_N_pos.
 
 Instance Op_N_add : BinOp N.add :=
   {| TBOp := Z.add ; TBOpInj := N2Z.inj_add |}.
-Add BinOp Op_N_add.
+Add Zify BinOp Op_N_add.
 
 Instance Op_N_min : BinOp N.min :=
   {| TBOp := Z.min ; TBOpInj := N2Z.inj_min |}.
-Add BinOp Op_N_min.
+Add Zify BinOp Op_N_min.
 
 Instance Op_N_max : BinOp N.max :=
   {| TBOp := Z.max ; TBOpInj := N2Z.inj_max |}.
-Add BinOp Op_N_max.
+Add Zify BinOp Op_N_max.
 
 Instance Op_N_mul : BinOp N.mul :=
   {| TBOp := Z.mul ; TBOpInj := N2Z.inj_mul |}.
-Add BinOp Op_N_mul.
+Add Zify BinOp Op_N_mul.
 
 Instance Op_N_sub : BinOp N.sub :=
   {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}.
-Add BinOp Op_N_sub.
+Add Zify BinOp Op_N_sub.
 
 Instance Op_N_div : BinOp N.div :=
   {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}.
-Add BinOp Op_N_div.
+Add Zify BinOp Op_N_div.
 
 Instance Op_N_mod : BinOp N.modulo :=
   {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}.
-Add BinOp Op_N_mod.
+Add Zify BinOp Op_N_mod.
 
 Instance Op_N_pred : UnOp N.pred :=
   { TUOp := fun x  => Z.max 0 (x - 1) ;
     TUOpInj :=
       ltac:(intros; rewrite N.pred_sub; apply N2Z.inj_sub_max) }.
-Add UnOp Op_N_pred.
+Add Zify UnOp Op_N_pred.
 
 Instance Op_N_succ : UnOp N.succ :=
   {| TUOp := fun x => x + 1 ; TUOpInj := N2Z.inj_succ |}.
-Add UnOp Op_N_succ.
+Add Zify UnOp Op_N_succ.
 
 (** Support for Z - injected to itself *)
 
 (* zify_Z_rel *)
 Instance Op_Z_ge : BinRel Z.ge :=
   {| TR := Z.ge ; TRInj := fun x y  => iff_refl (x>= y)|}.
-Add BinRel Op_Z_ge.
+Add Zify BinRel Op_Z_ge.
 
 Instance Op_Z_lt : BinRel Z.lt :=
   {| TR := Z.lt ;  TRInj := fun x y  => iff_refl (x < y)|}.
-Add BinRel Op_Z_lt.
+Add Zify BinRel Op_Z_lt.
 
 Instance Op_Z_gt : BinRel Z.gt :=
   {| TR := Z.gt ;TRInj := fun x y  => iff_refl (x > y)|}.
-Add BinRel Op_Z_gt.
+Add Zify BinRel Op_Z_gt.
 
 Instance Op_Z_le : BinRel Z.le :=
   {| TR := Z.le ;TRInj := fun x y  => iff_refl (x <= y)|}.
-Add BinRel Op_Z_le.
+Add Zify BinRel Op_Z_le.
 
 Instance Op_eqZ : BinRel (@eq Z) :=
   { TR := @eq Z ; TRInj := fun x y  => iff_refl (x = y) }.
-Add BinRel Op_eqZ.
+Add Zify BinRel Op_eqZ.
 
 Instance Op_Z_Z0 : CstOp Z0 :=
   { TCst := Z0  ; TCstInj := eq_refl }.
-Add CstOp Op_Z_Z0.
+Add Zify CstOp Op_Z_Z0.
 
 Instance Op_Z_add : BinOp Z.add :=
   { TBOp := Z.add  ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_add.
+Add Zify BinOp Op_Z_add.
 
 Instance Op_Z_min : BinOp Z.min :=
   { TBOp := Z.min ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_min.
+Add Zify BinOp Op_Z_min.
 
 Instance Op_Z_max : BinOp Z.max :=
   { TBOp := Z.max ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_max.
+Add Zify BinOp Op_Z_max.
 
 Instance Op_Z_mul : BinOp Z.mul :=
   { TBOp := Z.mul ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_mul.
+Add Zify BinOp Op_Z_mul.
 
 Instance Op_Z_sub : BinOp Z.sub :=
   { TBOp := Z.sub ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_sub.
+Add Zify BinOp Op_Z_sub.
 
 Instance Op_Z_div : BinOp Z.div :=
   { TBOp := Z.div ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_div.
+Add Zify BinOp Op_Z_div.
 
 Instance Op_Z_mod : BinOp Z.modulo :=
   { TBOp := Z.modulo ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_mod.
+Add Zify BinOp Op_Z_mod.
 
 Instance Op_Z_rem : BinOp Z.rem :=
   { TBOp := Z.rem ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_rem.
+Add Zify BinOp Op_Z_rem.
 
 Instance Op_Z_quot : BinOp Z.quot :=
   { TBOp := Z.quot ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_quot.
+Add Zify BinOp Op_Z_quot.
 
 Instance Op_Z_succ : UnOp Z.succ :=
   { TUOp := fun x => x + 1 ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_succ.
+Add Zify UnOp Op_Z_succ.
 
 Instance Op_Z_pred : UnOp Z.pred :=
   { TUOp := fun x => x - 1 ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_pred.
+Add Zify UnOp Op_Z_pred.
 
 Instance Op_Z_opp : UnOp Z.opp :=
   { TUOp := Z.opp ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_opp.
+Add Zify UnOp Op_Z_opp.
 
 Instance Op_Z_abs : UnOp Z.abs :=
   { TUOp := Z.abs ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_abs.
+Add Zify UnOp Op_Z_abs.
 
 Instance Op_Z_sgn : UnOp Z.sgn :=
   { TUOp := Z.sgn ; TUOpInj := ltac:(refl) }.
-Add UnOp Op_Z_sgn.
+Add Zify UnOp Op_Z_sgn.
 
 Instance Op_Z_pow : BinOp Z.pow :=
   { TBOp := Z.pow ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_pow.
+Add Zify BinOp Op_Z_pow.
 
 Instance Op_Z_pow_pos : BinOp Z.pow_pos :=
   { TBOp := Z.pow ; TBOpInj := ltac:(refl) }.
-Add BinOp Op_Z_pow_pos.
+Add Zify BinOp Op_Z_pow_pos.
 
 Instance Op_Z_double : UnOp Z.double :=
   { TUOp := Z.mul 2 ; TUOpInj := Z.double_spec }.
-Add UnOp Op_Z_double.
+Add Zify UnOp Op_Z_double.
 
 Instance Op_Z_pred_double : UnOp Z.pred_double :=
   { TUOp := fun x => 2 * x - 1 ; TUOpInj := Z.pred_double_spec }.
-Add UnOp Op_Z_pred_double.
+Add Zify UnOp Op_Z_pred_double.
 
 Instance Op_Z_succ_double : UnOp Z.succ_double :=
   { TUOp := fun x => 2 * x + 1 ; TUOpInj := Z.succ_double_spec }.
-Add UnOp Op_Z_succ_double.
+Add Zify UnOp Op_Z_succ_double.
 
 Instance Op_Z_square : UnOp Z.square :=
   { TUOp := fun x => x * x ; TUOpInj := Z.square_spec }.
-Add UnOp Op_Z_square.
+Add Zify UnOp Op_Z_square.
 
 Instance Op_Z_div2 : UnOp Z.div2 :=
   { TUOp := fun x => x / 2 ; TUOpInj := Z.div2_div }.
-Add UnOp Op_Z_div2.
+Add Zify UnOp Op_Z_div2.
 
 Instance Op_Z_quot2 : UnOp Z.quot2 :=
   { TUOp := fun x => Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }.
-Add UnOp Op_Z_quot2.
+Add Zify UnOp Op_Z_quot2.
 
 Lemma of_nat_to_nat_eq : forall x,  Z.of_nat (Z.to_nat x) = Z.max 0 x.
 Proof.
@@ -455,28 +455,28 @@ Qed.
 
 Instance Op_Z_to_nat : UnOp Z.to_nat :=
   { TUOp := fun x => Z.max 0 x ; TUOpInj := of_nat_to_nat_eq }.
-Add UnOp Op_Z_to_nat.
+Add Zify UnOp Op_Z_to_nat.
 
 (** Specification of derived operators over Z *)
 
 Instance ZmaxSpec : BinOpSpec Z.max :=
   {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}.
-Add BinOpSpec ZmaxSpec.
+Add Zify BinOpSpec ZmaxSpec.
 
 Instance ZminSpec : BinOpSpec Z.min :=
   {| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ;
      BSpec := Z.min_spec |}.
-Add BinOpSpec ZminSpec.
+Add Zify BinOpSpec ZminSpec.
 
 Instance ZsgnSpec : UnOpSpec Z.sgn :=
   {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ;
      USpec := Z.sgn_spec|}.
-Add UnOpSpec ZsgnSpec.
+Add Zify UnOpSpec ZsgnSpec.
 
 Instance ZabsSpec : UnOpSpec Z.abs :=
   {| UPred := fun n r: Z =>  0 <= n /\ r = n \/ n < 0 /\ r = - n ;
      USpec := Z.abs_spec|}.
-Add UnOpSpec ZabsSpec.
+Add Zify UnOpSpec ZabsSpec.
 
 (** Saturate positivity constraints *)
 
@@ -487,7 +487,7 @@ Instance SatProd : Saturate Z.mul :=
     PRes  := fun r => 0 <= r;
     SatOk := Z.mul_nonneg_nonneg
   |}.
-Add Saturate SatProd.
+Add Zify Saturate SatProd.
 
 Instance SatProdPos : Saturate Z.mul :=
   {|
@@ -496,7 +496,7 @@ Instance SatProdPos : Saturate Z.mul :=
     PRes  := fun r => 0 < r;
     SatOk := Z.mul_pos_pos
   |}.
-Add Saturate SatProdPos.
+Add Zify Saturate SatProdPos.
 
 Lemma pow_pos_strict :
   forall a b,
@@ -515,4 +515,4 @@ Instance SatPowPos : Saturate Z.pow :=
     PRes  := fun r => 0 < r;
     SatOk := pow_pos_strict
   |}.
-Add Saturate SatPowPos.
+Add Zify Saturate SatPowPos.