Fixing an interpretation bug with tactics in notations. For some obscure reason, Ltac interpretation does not allow tactics of the following shape : let x := bla in TacGeneric tac. Hence we force genargs to be tactics and build the resulting hole tactic from scratch.
Fixing an interpretation bug with tactics in notations. For some obscure
reason, Ltac interpretation does not allow tactics of the following
shape : let x := bla in TacGeneric tac. Hence we force genargs to be
tactics and build the resulting hole tactic from scratch.

TOSPIO/coq,ejgallego/coq,letouzey/coq-wip,pirapira/coq2rust,silene/coq,8l/coq,SkySkimmer/coq,ale-f/coq,gares/coq,letouzey/coq-wip,Zimmi48/coq,amintimany/coq,william-lawvere/coq,SkySkimmer/coq,ppedrot/coq,ejgallego/coq,Ptival/coq,ppedrot/coq,gares/coq,gmalecha/coq,TheTypoMaster/coq,JasonGross/coq,william-lawvere/coq,mattam82/coq,silene/coq,maximedenes/coq,SkySkimmer/coq,gmalecha/coq,letouzey/coq-wip,Ptival/coq,amintimany/coq,Lionel-Rieg/coq,TheTypoMaster/coq,herbelin/github-coq,shindere/coq,pirapira/coq2rust,ale-f/coq,ale-f/coq,jpdeplaix/coq,barras/coq,shindere/coq,ejgallego/coq,8l/coq,Matafou/coq,jpdeplaix/coq,maximedenes/coq,pirbo/coq,silene/coq,Zimmi48/coq,william-lawvere/coq,ppedrot/coq,ejgallego/coq,gares/coq,jpdeplaix/coq,JasonGross/coq,herbelin/github-coq,barras/coq,pirbo/coq,Matafou/coq,barras/coq,TheTypoMaster/coq,asr/coq,coq/coq,mattam82/coq,amintimany/coq,asr/coq,Lionel-Rieg/coq,Zimmi48/coq,maximedenes/coq,coq/coq,mattam82/coq,shindere/coq,ppedrot/coq,coq/coq,pirapira/coq2rust,Matafou/coq,Ptival/coq,mlasson/coq,SkySkimmer/coq,asr/coq,gares/coq,maximedenes/coq,JasonGross/coq,JasonGross/coq,herbelin/github-coq,aspiwack/coq,mlasson/coq,TOSPIO/coq,aspiwack/coq,Zimmi48/coq,Lionel-Rieg/coq,8l/coq,aspiwack/coq,ppedrot/coq,maximedenes/coq,gares/coq,letouzey/coq-wip,pirbo/coq,TOSPIO/coq,letouzey/coq-wip,gmalecha/coq,coq/coq,mlasson/coq