Is there a way to get generalized rewriting with stratagies to interact with ltac backtracking? Asked differently: is there any way to get the following to succeed?

```
From Coq Require Import Setoid.
Axiom lem1 : False -> 1+1=2.
Axiom lem2 : True -> 1+1=2.
Goal 1+1=2. (rewrite_strat subterms (choice lem1 lem2)); exact I. Qed.
```

I don't think rewrite_strat is a multi success tactic yes, but can certainly be turned into one (it's based on continuations already)

I suppose now I understand what a multi-success tactic is. Thanks! :)

Could you give an estimate of what would be involved in making this change (or providing a separate version of `rewrite_strat`

)?

Last updated: Jun 18 2024 at 00:02 UTC