coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix make_exact_entry to allow applying [forall x, P x] hints directly,	msozeau	2009-12-01
*	Correction du bug #2118 (Coqdep does not escape #)	notin	2009-11-19
*	Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions...	notin	2009-11-12
*	Correction du bug #2183	notin	2009-11-10
*	Misc fixes.	msozeau	2009-11-06
*	Correction du bug #2153 (-D n'est pas une option standard de install)	notin	2009-11-05
*	Removed debugging stuff mistakenly introduced in r12426.	herbelin	2009-11-03
*	Removed 'dest' from keyword highlighting.	gmelquio	2009-10-30
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Add a new vernacular command for controling implicit generalization of	msozeau	2009-10-27
*	Added option --external to coqdoc to bind an url to an external library.	herbelin	2009-10-27
*	Better handling of emphasis.	msozeau	2009-10-13
*	Add support for Local Declare ML Module	glondu	2009-09-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Tentatively made order-dependency wrt .vo files a full dependency	herbelin	2009-09-15
*	Fixes for toc depth handling and handling of substitles from Chris Casinghino.	msozeau	2009-09-10
*	Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch	msozeau	2009-09-08
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,	msozeau	2009-09-04
*	Add --plain-comments patch by F. Garillot, which also adds	msozeau	2009-09-03
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Allow coqdoc comments inside definition bodies.	msozeau	2009-07-09
*	Adapted the emacs mode to font-lock. Re-using code from ProofGeneral.	courtieu	2009-05-28
*	Report de la révision #12104 (Maj lien site web de Coq)	notin	2009-04-24
*	Take formatted into account in rules for dot.	msozeau	2009-04-08
*	Change HTML paragraph output to avoid too much space after bulleted	msozeau	2009-04-08
*	Fix behavior on newlines with parse-comments and also do [] escaping as	msozeau	2009-04-06
*	Coqdep: some dead code and code move (first experiment with Oug)	letouzey	2009-03-27
*	Coqdep_boot: one line with bad indentation	letouzey	2009-03-26
*	Protect typeset arguments in titles in LaTeX output (fixes compilation	msozeau	2009-03-26
*	Fix coqdoc bugs reported by Ian Lynagh.	msozeau	2009-03-24
*	pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)	letouzey	2009-03-24
*	More elaborate handling of newlines in Gallina mode. Support inline	msozeau	2009-03-22
*	coqdoc fixes and support for parsing regular comments (request by	msozeau	2009-03-22
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20
*	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras	2009-03-19
*	coq_makefile: no ml dependency on coq sources	barras	2009-03-18
*	- configure: affiche si le natdynlink est positionne	barras	2009-03-17
*	missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was includ...	barras	2009-03-16
*	coqdep_boot: a specialized and dependency-free coqdep for killing one of the ...	letouzey	2009-03-16
*	Coqdep: better handling of Declare ML Module (via .mllib) + many cleanups	letouzey	2009-03-14
*	Coqdep: remove references to obsolete .zi and Require Implementation stuff	letouzey	2009-03-14
*	Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module name	letouzey	2009-03-11
*	Amélioration de coq_makefile	notin	2009-02-24
*	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin	2009-02-11
*	From v8.2 to trunk:	herbelin	2009-02-06
*	Fix d'un bug avec l'option gallina	notin	2009-02-04
*	- Better deal with commands inside section titles in latex output using	msozeau	2009-01-21
*	Various little fixes:	msozeau	2009-01-18