coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Getting rid of the previous implementation of setoid_rewrite which was	msozeau	2009-01-18
*	Last changes in type class syntax:	msozeau	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	Correct a bug in commit 11659	puech	2009-01-16
*	Patch by Brian Campbell to output more information on the exception that	msozeau	2009-01-15
*	Fixing #1960 (xml bug with external on goal variable) and #1961	herbelin	2009-01-14
*	Fixing/improving management of uniform prefix Local and Global	herbelin	2009-01-14
*	Updated dates	herbelin	2009-01-13
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	Workaround to compile the coq archive with dynamic loading on Mac OS 10.5	herbelin	2009-01-13
*	Fix a bunch of bugs related to setoid_rewrite, unification and evars:	msozeau	2009-01-12
*	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin	2009-01-11
*	Another problem with blanks in filenames	herbelin	2009-01-10
*	- Fixed the recompilation of config/revision.ml once every two conmpilations.	herbelin	2009-01-10
*	Oups... il n'y a pas d'option -impl pour ocamldep	notin	2009-01-09
*	Remove trailing newlines in outputs of X -where	glondu	2009-01-08
*	Minor doc fixes:	msozeau	2009-01-08
*	Uniformisation of some error messages + added test on setoid rewrite.	herbelin	2009-01-07
*	Fixing a cosmetic tactic printer bug in passing	herbelin	2009-01-07
*	Sous Windows, 'coqtop -where' renvoit des chemins contenant des '\'	notin	2009-01-07
*	Fix build for git users	glondu	2009-01-07
*	Suite de la révision #11756	notin	2009-01-07
*	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...	notin	2009-01-06
*	Report de la révision 11754 (compilation sous windows)	notin	2009-01-06
*	Installation des librairies: on utilise maintenant LINKCMO au lieu de	notin	2009-01-06
*	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin	2009-01-05
*	Added installation of .cmi files in "make install" target of coq_makefile.	herbelin	2009-01-04
*	Moved JProver to a user contribution (as was decided a long time ago)	herbelin	2009-01-04
*	Bug dans commit 11743	herbelin	2009-01-04
*	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin	2009-01-04
*	Fixed two problems:	herbelin	2009-01-03
*	Regression test for bug #1967	herbelin	2009-01-02
*	Conséquence renommage canonique de refl_equal en eq_refl.	herbelin	2009-01-02
*	Made the debugger work again:	herbelin	2009-01-02
*	Fixed two apparent inconsistencies in matching.ml:	herbelin	2009-01-02
*	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin	2009-01-02
*	Update	herbelin	2009-01-01
*	Switched to "standardized" names for the properties of eq and	herbelin	2009-01-01
*	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin	2009-01-01
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	Produce better html code with coqdoc and improve doc:	msozeau	2008-12-29
*	compatibility with lablgtk2 version 2.12	bertot	2008-12-29
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	FMaps: various updates (mostly suggested by P. Casteran)	letouzey	2008-12-26
*	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin	2008-12-26
*	11715 continued	herbelin	2008-12-26
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	- Suppression date dans configure du trunk	herbelin	2008-12-26