adds the possibility to have terms (and not just identifiers) as hints Adds the 'Reserved Notation' command
adds the possibility to have terms (and not just identifiers) as hints
Adds the 'Reserved Notation' command


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

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