strengthened solve_decision ltac

@aa755 thanks for the MR!

Could you give an example for the kind of goal this helps with? The choice of not making this tactic recursive was deliberate, I think. (Never mind I confused this tactic with another one.)

Also, if this does solve more goals (and it does not cost too much performance or have other reasons we might prefer the old tactic), there should be a testcase added (probably in tests/tactics.v) to ensure such goals remain solvable as the tactic evolves.

The choice of not making this tactic recursive was deliberate, I think.

Yes, it was deliberate, because failure usually means that another Decision instance is missing.

If you have a hierachy of inductive data types (say, base_lit, bin_op, val, expr in HeapLang), you want to have a Decision instance for all of them.

If you really want to have the recursive behavior at some particular place (where it's really not relevant to have Decision instances for data types lower in the hierarchy), better just use repeat solve_decision there.

Thanks for the review. I agree that it is better to just add the intermediate instances. I wish ltacs could declare new instances.

closed