Notations can now accept dummy arguments. If ever a bound variable is not
used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.
Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at
internalization time.
Notation variables are now taken into account as possible ltac bound variables
when internalizing a term.
Adding a finer-grained -bt flag to coqtop only triggering backtraces.
Adding -bt to coqc.
Slight code cleaning ensuring more static invariants in Rewrite.
Do not pass unification flags around in Rewrite.
Rewrite.ml: removing direction flag from hypinfo.