coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	pushed evar reduction in kernel	barras	2009-02-06
*	Forgot a file in r11859. Sorry...	puech	2009-01-27
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	Getting rid of the previous implementation of setoid_rewrite which was	msozeau	2009-01-18
*	DISCLAIMER	puech	2009-01-17
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	11715 continued	herbelin	2008-12-26
*	- coq_makefile: target install now respects the original tree structure	herbelin	2008-12-24
*	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin	2008-12-19
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	About "apply in":	herbelin	2008-12-09
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ	herbelin	2008-11-05
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau	2008-10-23
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Generalized implementation of generalization.	msozeau	2008-10-23
*	Affichage des notations récursives:	herbelin	2008-10-22
*	Suite 11472	herbelin	2008-10-19
*	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin	2008-10-11
*	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau	2008-09-15
*	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau	2008-09-07
*	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau	2008-09-07
*	- New auto hints for transparency/opacity control, not bound to	msozeau	2008-08-22
*	Correction de bugs:	herbelin	2008-08-05
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18
*	Correction bug "parser" suite changement syntaxe	herbelin	2008-06-29
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	Add possibility to match on defined hypotheses, using brackets to	msozeau	2008-06-16
*	Correction parser révélé par test-suite	herbelin	2008-06-12
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	Strategy commands are now exported	barras	2008-05-22
*	refined the conversion oracle	barras	2008-05-21
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	Autre oubli de la révision 10904	herbelin	2008-05-08
*	Postpone the search for the recursive argument index from the user given	msozeau	2008-05-06
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	- Add "Global" modifier for instances inside sections with the usual	msozeau	2008-04-15
*	oubli sur 10790	herbelin	2008-04-14
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13