Merge PR #11370: [zify] elim let in ML

Reviewed-by: ppedrot

4 files changed, 43 insertions, 3 deletions

diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v
index 785a53fafa..18cd196148 100644
--- a/plugins/micromega/Zify.v
+++ b/plugins/micromega/Zify.v
@@ -87,4 +87,4 @@ Ltac applySpec S :=
 (** [zify_post_hook] is there to be redefined. *)
 Ltac zify_post_hook := idtac.
 
-Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook.
+Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook.
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 66f263c0b1..2b5fac32a2 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -34,12 +34,13 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
 END
 
 TACTIC EXTEND ITER
-| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t }
+| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t }
 END
 
 TACTIC EXTEND TRANS
 | [ "zify_op"  ] -> { Zify.zify_tac }
-| [ "saturate"  ] -> { Zify.saturate }
+| [ "zify_saturate"  ] -> { Zify.saturate }
+| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t }
 END
 
 VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 5d8ae83853..e71c89b4db 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -965,6 +965,43 @@ let trans_concl t =
 let tclTHENOpt e tac tac' =
   match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac'
 
+let assert_inj t =
+  init_cache ();
+  Proofview.Goal.enter (fun gl ->
+      let env = Tacmach.New.pf_env gl in
+      let evd = Tacmach.New.project gl in
+      try
+        ignore (get_injection env evd t);
+        Tacticals.New.tclIDTAC
+      with Not_found ->
+        Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist"))
+
+let do_let tac (h : Constr.named_declaration) =
+  match h with
+  | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC
+  | Context.Named.Declaration.LocalDef (id, t, ty) ->
+    Proofview.Goal.enter (fun gl ->
+        let env = Tacmach.New.pf_env gl in
+        let evd = Tacmach.New.project gl in
+        try
+          ignore (get_injection env evd (EConstr.of_constr ty));
+          tac id.Context.binder_name t ty
+        with Not_found -> Tacticals.New.tclIDTAC)
+
+let iter_let tac =
+  Proofview.Goal.enter (fun gl ->
+      let env = Tacmach.New.pf_env gl in
+      let sign = Environ.named_context env in
+      Tacticals.New.tclMAP (do_let tac) sign)
+
+let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) =
+  init_cache ();
+  iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) ->
+      Ltac_plugin.Tacinterp.Value.apply tac
+        [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id)
+        ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t)
+        ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ])
+
 let zify_tac =
   Proofview.Goal.enter (fun gl ->
       Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"];
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 9e3cf5d24c..4930a845c9 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -27,3 +27,5 @@ module Saturate : S
 val zify_tac : unit Proofview.tactic
 val saturate : unit Proofview.tactic
 val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic
+val assert_inj : EConstr.constr -> unit Proofview.tactic
+val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic