coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	Correction problème de compil (blast.ml)	herbelin	2008-04-04
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin	2008-04-01
*	Suite commit 10730: MAJ xlate.ml	herbelin	2008-03-30
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Rework on rich forms of rewrite	letouzey	2008-03-01
*	Forgotten file in previous commit	lmamane	2008-02-25
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Change notation for setoid inequality, coerce objects before comparing them. ...	msozeau	2008-01-18
*	Completion of 10427...	herbelin	2008-01-07
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Nettoyage de Print Assumptions :	aspiwack	2007-11-09
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Complément nécessaire aux révisions 10156 et 10157	herbelin	2007-10-01
*	Modification of the Scheme command.	vsiles	2007-09-28
*	Oubli dans commit 10102...	herbelin	2007-08-30
*	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin	2007-08-27
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27