From 4da8f114155d2abb31ce8a45a2f17f21f7d97a0e Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 10 Aug 2020 15:31:58 +0200
Subject: [zify] fix for bug#12791

The elimination of let bindings is performing a convertibility check in
order to deal with type aliases.
---
 plugins/micromega/zify.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'plugins')

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 =
-- 
cgit v1.2.3