Commit f8adf66f authored by Abhishek Anand's avatar Abhishek Anand
Browse files

strengthened solve_decision ltac

parent 7b2056c4
Pipeline #50364 passed with stage
in 9 minutes and 39 seconds
......@@ -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. *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment