Skip to content
Snippets Groups Projects

strengthened solve_decision ltac

Closed strengthened solve_decision ltac
aa755/stdpp:aa755-master-patch-77362 into master
Closed Abhishek Anand requested to merge aa755/stdpp:aa755-master-patch-77362 into master
Viewing commit f8adf66f
Show latest version
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
theories/decidable.v
+ 1
− 1
@@ -66,7 +66,7 @@ Ltac solve_trivial_decision :=
Ltac solve_decision :=
unfold EqDecision; intros; first
[ solve_trivial_decision
| unfold Decision; decide equality; solve_trivial_decision ].
| unfold Decision; decide equality; solve_decision ].
(** The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)