Update zify documentation

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

2 files changed, 44 insertions, 19 deletions

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')