| Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot
for porting this chapter.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Work done by Assia Mahboubi and Enrico Tassi
|
|
This commit removes from the source tree plugins/decl_mode,
its chapter in the reference manual and related tests.
|
|
|
|
|
|
Also remove AsyncProofs.tex from the list of preprocessed files, as it is
doubtful it will ever contains Coq scripts.
|
|
|
|
|
|
|
|
Putting utf8 everywhere helps the maintainance of the online refman.
And anyway, this is the way to go. We should also chase and migrate
the few remaining iso-latin-1 files elsewhere in the sources.
|
|
|
|
|
|
|
|
I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.
|
|
|
|
This encompasses commits r15183, r15190, r15243, r15262, r15276, r15277,
r15278, r15337. The merge did not go without troubles, but hopefully none
of the changes were lost in process.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15806 85f007b7-540e-0410-9357-904b9bb8a0f7
|