Commit 28653f29 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bug in naive_solver.

parent dfa4c3ba
......@@ -333,7 +333,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
| H : False |- _ => destruct H
| H : _ _ |- _ => destruct H
| H : _, _ |- _ => destruct H
| H : ?P ?Q, H2 : ?Q |- _ => specialize (H H2)
| H : ?P ?Q, H2 : ?P |- _ => specialize (H H2)
(**i simplify and solve equalities *)
| |- _ => progress simplify_equality'
(**i solve the goal *)
......
Markdown is supported
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