Bugs de vérification de la bonne fondation en présence de définitions locales dans le type de l'inductif décroissant
Bugs de vérification de la bonne fondation en présence de définitions locales dans le type de l'inductif décroissant


git-svn-id: 44dc50bdcc0f5d1a212c497508dc9452e0b35e2b@2099 85f007b7-540e-0410-9357-904b9bb8a0f7

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