From bcd963fb43b08f5154d4891845292524e2cad02e Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 1 Aug 2016 15:07:17 -0700
Subject: Better transparency of dec_eq_sig_hprop

---
 src/Util/Decidable.v | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

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

diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index 20ec7f0c9..2aac1759b 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -46,18 +46,21 @@ Ltac pre_decide_destruct_sigma := repeat pre_decide_destruct_sigma_step.
 
 Ltac pre_decide :=
   repeat (intros
-          || subst
           || destruct_decidable
           || split
           || pre_decide_destruct_sigma
           || unfold Decidable in *
-          || hnf
+          || hnf).
+
+Ltac post_decide :=
+  repeat (intros
+          || subst
           || pre_hprop).
 
 Ltac solve_decidable_transparent_with tac :=
   pre_decide;
-  try solve [ left; abstract tac
-            | right; abstract tac
+  try solve [ left; abstract (post_decide; tac)
+            | right; abstract (post_decide; tac)
             | decide equality; eauto with nocore ].
 
 Ltac solve_decidable_transparent := solve_decidable_transparent_with firstorder.
-- 
cgit v1.2.3