Merge PR #12814: [zify] fix for bug#12791

Reviewed-by: vbgl

1 files changed, 8 insertions, 3 deletions

diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 4e1f9a66ac..fa29e6080e 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) =
         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 (EConstr.of_constr t)
-            (EConstr.of_constr ty)
+          let x = id.Context.binder_name in
+          ignore
+            (let eq = Lazy.force eq in
+             find_option
+               (match_operator env evd eq
+                  [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|])
+               (HConstr.find_all eq !table_cache));
+          tac x (EConstr.of_constr t) (EConstr.of_constr ty)
         with Not_found -> Tacticals.New.tclIDTAC)
 
 let iter_let_aux tac =