Compatibility ocaml 3.12.
Simplifying second_order_matching: no need to invert the linear
initial segment of the context of the evar.
Fixing #3892: Ensure that notation variables do not capture names
hidden behind another notation.