Hi everyone,

I am trying to implement a tactic that uses small hint databases to solve simple arithmetic problems:

```
Ltac pattern_matching_rewriter :=
match goal with
|[ |- context[0] ] => solve[auto with nocore zero_rewriters]
|[ |- context[1] ] => solve[auto with nocore one_rewriters]
|[ |- context[- _] ] => solve[auto with nocore opp_rewriters]
|[ |- context[Rabs _] ] => solve[auto with nocore abs_rewriters]
|[ |- context[R_dist _] ] => solve[auto with nocore abs_rewriters]
|[ |- context[_²] ] => solve[auto with nocore sqr_rewriters]
|[ |- context[exp _] ] => solve[auto with nocore exp_rewriters]
|[ |- context[_ + _]] => solve[auto with nocore plus]
|[ |- context[_ - _]] => solve[auto with nocore minus]
|[ |- context[_ * _]] => solve[auto with nocore mult]
| _ => first[solve[timeout 5 auto with nocore rewriters] | idtac "Finding a proof takes too long. Try taking a smaller step."]
end.
```

So for example, whenever the goal contains an exponential, I want to use the `exp_rewriters`

database. However, sometimes, my goal contains an exponential and a square. In that case I would like to use both the `exp_rewriters`

as well as the `abs_rewriters`

databases , without using all of the others (the rewriters database contains all databases).

Is there a possibility to do that, without hardcoding every possible combination?

Thanks in advance!