Commit a426377a by Robbert

### Merge branch 'ci/robbert/naive_solver' into 'master'

Perform `fast_done` first in `naive_solver`.

See merge request !80
parents 3c3ba0dd f87c334f
Pipeline #17984 passed with stage
in 9 minutes and 3 seconds
 ... @@ -506,6 +506,8 @@ Tactic Notation "naive_solver" tactic(tac) := ... @@ -506,6 +506,8 @@ Tactic Notation "naive_solver" tactic(tac) := end; end; let rec go n := let rec go n := repeat match goal with repeat match goal with (**i solve the goal *) | |- _ => fast_done (**i intros *) (**i intros *) | |- ∀ _, _ => intro | |- ∀ _, _ => intro (**i simplification of assumptions *) (**i simplification of assumptions *) ... @@ -522,8 +524,6 @@ Tactic Notation "naive_solver" tactic(tac) := ... @@ -522,8 +524,6 @@ Tactic Notation "naive_solver" tactic(tac) := | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H (**i simplify and solve equalities *) (**i simplify and solve equalities *) | |- _ => progress simplify_eq/= | |- _ => progress simplify_eq/= (**i solve the goal *) | |- _ => fast_done (**i operations that generate more subgoals *) (**i operations that generate more subgoals *) | |- _ ∧ _ => split | |- _ ∧ _ => split | |- Is_true (bool_decide _) => apply (bool_decide_pack _) | |- Is_true (bool_decide _) => apply (bool_decide_pack _) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!