Deducteam
Improve scoping of pattern variables not used in the RHS
The first argument of the Patt data type is an integer option which was once set to None at scoping if the variable was linear and not used in the right hand side, like in
rule $X $Y --> $Y
the variable $X was transformed to Patt(None, "X", [||]) and $Y to Patt(Some(i), "Y", [||]), where i would probably be 1.
Compilation to decision trees relies on the form of this argument for optimisation (it doesn't impact correctness): if the first argument is set to None, than there is no need to remember the subterm matched by the pattern, and it can hence be discarded.
Nowadays, the first argument of patterns is always of the form Some i after scoping. Therefore decision trees backup more terms than needed.
Note that the fact that there is currently no Patt(None,_,_) is used for computing critical pairs.
