coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertance	soubiran	2008-04-23
*	correction bug 1839	soubiran	2008-04-22
*	fixed universes bug related to module inclusion	barras	2008-04-22
*	added the .vo checker (with independent Makefile)	barras	2008-04-21
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Correction bug 1838 + doc modules.	soubiran	2008-04-21
*	Add the ability to give a transparent_state for conversion, to	msozeau	2008-04-20
*	suite 10790 (identificateurs)	herbelin	2008-04-14
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Patch sur le typage d'un foncteur applique a un alias.	soubiran	2008-04-03
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...	soubiran	2008-03-26
*	Correction de bugs relatifs a la compostion des substitutions	soubiran	2008-03-25
*	improved the implementation of rtree	barras	2008-03-18
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0...	barras	2008-03-18
*	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin	2008-03-15
*	Ajout des alias de module dans le noyau.	soubiran	2008-03-14
*	fold travaille maintenant sur la forme beta-iota-zeta réduite du	herbelin	2008-03-10
*	Fix a few bugs in Program: use user-given typing constraints for	msozeau	2008-03-09
*	Attempt of fix for extraction of modules types	letouzey	2008-03-05
*	patch for C code of addmuldiv31	thery	2008-02-27
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Patch bug #1799	soubiran	2008-02-15
*	Add more information to IllFormedRecBody exceptions, to show the exact	msozeau	2008-02-08
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Finish let\| implementation and document it	msozeau	2008-01-31
*	bug in accessing n-th abstraction	barras	2008-01-18
*	Fixed bug 1761 (unexpected anomaly when constructor type has invalid	herbelin	2008-01-05
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack	2007-12-18
*	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
*	bug in infos_and_sort: type of constructor was not reduced enough	barras	2007-11-07
*	bug in safe_typing: univ constraints generated by section variables were not ...	barras	2007-10-30
*	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin	2007-10-04
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	normalisation (by closure) was not performed under fixpoints	barras	2007-07-12
*	kill an ugly warning about a non-exhaustive pattern	letouzey	2007-06-26
*	Correction de plusieurs bugs de l'export XML (utilisation d'un type de	herbelin	2007-06-21
*	ajout de head0 et tail0 en natif	bgregoir	2007-06-20
*	Corrections dans le Print Assumption. Les definitions locales ("Let")	aspiwack	2007-05-30
*	Memory optimisation for modules and constrs substitutions.	soubiran	2007-05-30
*	Correction of (PR#1576).	soubiran	2007-05-25
*	Suite restructuration unification et division des problèmes	herbelin	2007-05-23
*	Nettoyage et standardisation des messages d'erreurs.	herbelin	2007-05-17
*	corrections bug dans l'implem de int31	bgregoir	2007-05-15
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11