From 1595e35f97a68d6672ae59c75a6324c830888130 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Tue, 2 Apr 2019 22:58:00 +0200
Subject: [PATCH] Avoid conversion after only reducing goal.

---
 theories/proofmode/reduction.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 0db1e202a..0e81f651f 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -20,7 +20,7 @@ Declare Reduction pm_eval := cbv [
 Ltac pm_eval t :=
   eval pm_eval in t.
 Ltac pm_reduce :=
-  match goal with |- ?u => let v := pm_eval u in change v end.
+  match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
 
 (** Called by many tactics for redexes that are created by instantiation.
@@ -34,4 +34,4 @@ Declare Reduction pm_prettify := cbn [
   bi_tforall bi_texist
 ].
 Ltac pm_prettify :=
-  match goal with |- ?u => let v := eval pm_prettify in u in change v end.
+  match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.
-- 
GitLab