CompSpec2Type is used to build functions, it should be Defined, not Qed
CompSpec2Type is used to build functions, it should be Defined, not Qed

  This solves in particular the compilation failure of contrib ATBR

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

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