diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 0db1e202a4da65b2c6275ec641b4a69a9941ecf2..173894c20be93ca85772fda37ae3055900cee66e 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.