diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-01 15:07:17 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-01 15:07:17 -0700 |
| commit | bcd963fb43b08f5154d4891845292524e2cad02e (patch) | |
| tree | c194ed59f6abf377d616d1bc4fda43dcbe1e7f7a /src/Util/Decidable.v | |
| parent | 900cbe7e50da8ad0f52844bf789fc1a5e75d0756 (diff) | |
Better transparency of dec_eq_sig_hprop
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 11 |
1 files changed, 7 insertions, 4 deletions
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. |