From c462b6e63b2fd829f3013a38446fcf5f6ee7bcd7 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 1 Aug 2016 15:09:42 -0700
Subject: Add a comment

---
 src/Util/Decidable.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Util/Decidable.v')

diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index 2aac1759b..8488ad303 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -52,6 +52,9 @@ Ltac pre_decide :=
           || unfold Decidable in *
           || hnf).
 
+(** Put the [subst] and reasoning about equalities after the [left]
+    and [right]; opaque equality proofs should not block decidability
+    proofs. *)
 Ltac post_decide :=
   repeat (intros
           || subst
-- 
cgit v1.2.3