coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	I forgot a line in previous commit.	aspiwack	2012-06-22
*	A call to the command Proof (and its variants) now prints the subgoals.	aspiwack	2012-06-22
*	Fixed #2821.	ppedrot	2012-06-21
*	Fixing #2825.	ppedrot	2012-06-21
*	Fix bug #2808: wrong handling of evars in Instance command.	msozeau	2012-06-21
*	Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:	msozeau	2012-06-21
*	Fixing accelerator dynamic modification in CoqIDE.	ppedrot	2012-06-21
*	Fixing use of an error instead of a boolean result in the unification	herbelin	2012-06-20
*	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin	2012-06-20
*	Fixing bug #2809 (anomaly when printing a module with notations due to	herbelin	2012-06-20
*	Install compat5 module with grammar.cma	pboutill	2012-06-20
*	Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...	pboutill	2012-06-20
*	Bug 2823: update INSTALL.ide in order to ask for lablgtksourceview	pboutill	2012-06-20
*	Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri...	msozeau	2012-06-19
*	Fix bug #2695: infinite loop in dependent destruction.	msozeau	2012-06-19
*	BinInt: a forgotten scope for a notation	letouzey	2012-06-19
*	Fixing printing of @f with no arguments	herbelin	2012-06-19
*	Fixing some inconsistencies of constr printer wrt constr parser	herbelin	2012-06-19
*	Proof using: nested sections bugfix	gareuselesinge	2012-06-18
*	Reductionops abstract machine uses Zcase & Zfix stack node.	pboutill	2012-06-15
*	Reductionops : Better abstract machine stack utilities	pboutill	2012-06-15
*	Fix coqide vernac lexer	pboutill	2012-06-15
*	Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN	pboutill	2012-06-15
*	Constrextern is allow to use partially applied notations	pboutill	2012-06-14
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	coq_makefile fixup	pboutill	2012-06-14
*	Fixing annoying autocompletion when deleting text.	ppedrot	2012-06-13
*	make sure that documentation compilation works after adding files for	bertot	2012-06-12
*	New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles	pboutill	2012-06-12
*	bug 2805: Only export CAMLP4LIB if camlp4 -where ends successfully	pboutill	2012-06-12
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
*	Getting rid of Pcoq remains.	ppedrot	2012-06-12
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
*	These files are displaced from Rtrigo.v and Ranalysis_reg.v	bertot	2012-06-11
*	finish the rearrangement for removing the sin_PI2 axiom. This new version	bertot	2012-06-11
*	Adds the proof of PI_ineq, plus some other smarter ways to approximate PI	bertot	2012-06-11
*	Colorization of coqtop messages is turned off by default	letouzey	2012-06-07
*	CHANGES: mention the end of induction principles for records	letouzey	2012-06-05
*	Modifications and rearrangements to remove the action that sin (PI/2) = 1	bertot	2012-06-05
*	A box to pretty-print them all.	ppedrot	2012-06-04
*	Fixing previous commit (something strange happened...)	ppedrot	2012-06-04
*	Replacing some str with strbrk	ppedrot	2012-06-04
*	Added a color output to Coqtop.	ppedrot	2012-06-04
*	Separated notice vs info messages, and cleaned up the interface a bit.	ppedrot	2012-06-04
*	Fixing #2803.	ppedrot	2012-06-04
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Fixed printing error problem... A line had disappeared in a previous patch.	ppedrot	2012-06-02
*	Flushing formatters before program exit.	ppedrot	2012-06-02
*	More cleaning	ppedrot	2012-06-01
*	Cleaning Pp.ppnl use	ppedrot	2012-06-01