Preliminary work before adding general support for patterns in notations I.
Preliminary work before adding general support for patterns in notations I.

Factorizing the place where the different form of extended binders
(i.e. possibly including the 'pat form) are matched.

JasonGross/coq,SkySkimmer/coq,Matafou/coq,Matafou/coq,ejgallego/coq,JasonGross/coq,maximedenes/coq,coq/coq,JasonGross/coq,gares/coq,silene/coq,silene/coq,coq/coq,gares/coq,letouzey/coq-wip,silene/coq,coq/coq,gares/coq,coq/coq,ppedrot/coq,Matafou/coq,gares/coq,maximedenes/coq,ejgallego/coq,SkySkimmer/coq,maximedenes/coq,ppedrot/coq,letouzey/coq-wip,SkySkimmer/coq,ejgallego/coq,letouzey/coq-wip,letouzey/coq-wip,maximedenes/coq,ppedrot/coq,gares/coq,ejgallego/coq,ppedrot/coq,ppedrot/coq,Zimmi48/coq,Zimmi48/coq,letouzey/coq-wip,SkySkimmer/coq,Zimmi48/coq,Zimmi48/coq,maximedenes/coq,JasonGross/coq