From 46e7af84465f00b3547fdd9fafb6a7e89c764eb6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Apr 2019 09:47:33 +0200
Subject: [PATCH] Add comments.

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

diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 0e81f651f..1c4860221 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -20,6 +20,8 @@ Declare Reduction pm_eval := cbv [
 Ltac pm_eval t :=
   eval pm_eval in t.
 Ltac pm_reduce :=
+  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  conversion check twice. *)
   match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
 
@@ -34,4 +36,6 @@ Declare Reduction pm_prettify := cbn [
   bi_tforall bi_texist
 ].
 Ltac pm_prettify :=
+  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  conversion check twice. *)
   match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.
-- 
GitLab