coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Correction du bug #1819	notin	2008-04-01
*	- Fix for rewriting under dependent products.	msozeau	2008-03-31
*	Suite commit 10730: MAJ xlate.ml	herbelin	2008-03-30
*	Modifications diverses et variées :	herbelin	2008-03-30
*	Ajout d'abbréviations/notations paramétriques	herbelin	2008-03-30
*	Fix test-suite files, change conflicting notation "->rel" and the others	msozeau	2008-03-29
*	Improve error handling and messages for typeclasses.	msozeau	2008-03-28
*	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau	2008-03-28
*	Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression	notin	2008-03-28
*	- notations &&& and \|\|\| equivalent to andb and orb,	letouzey	2008-03-27
*	Various fixes on typeclasses:	msozeau	2008-03-27
*	Diverses petites modifs dans la test-suite:	notin	2008-03-26
*	Bug dans la gestion des dépendances vers les .ml	notin	2008-03-26
*	Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et coq_m...	notin	2008-03-26
*	Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...	soubiran	2008-03-26
*	Prise en compte des dépendances des .ml	notin	2008-03-25
*	Correction de bugs relatifs a la compostion des substitutions	soubiran	2008-03-25
*	Correction d'un bug dans la gestion des 'Declare ML Module'	notin	2008-03-25
*	Interpret patterns for hypotheses types in match goal in type_scope (if not a	msozeau	2008-03-25
*	Finish fix in command where we still lost information on what was a type	msozeau	2008-03-24
*	Fix examples in Program documentation and add comindexes for the various	msozeau	2008-03-23
*	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau	2008-03-23
*	Nettoyage Wf.v et unification (suite remarques faites sur cocorico)	herbelin	2008-03-23
*	Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.	herbelin	2008-03-23
*	Une passe sur les réels:	herbelin	2008-03-23
*	CoqIDE default font set to monospace so as indentation to be meaningful	herbelin	2008-03-23
*	Compatibility fixes, backtrack on definitions of reflexive,	msozeau	2008-03-22
*	One more AVL reorganisation: separate pure functions from proofs + functional...	letouzey	2008-03-21
*	Correct bug introduced in r10589, where we lost information that	msozeau	2008-03-21
*	Some "if then else" instead of orb and andb, in order to vm_compute lazily	letouzey	2008-03-21
*	Add a flag to control rewriting under lambdas. Otherwise makes some	msozeau	2008-03-20
*	Installation des .vo nécessaire à BigQ	notin	2008-03-20
*	Correction d'un bug sur les modules de la forme:	soubiran	2008-03-20
*	still some useless invariants in FSetAVL	letouzey	2008-03-20
*	some references to IntMap forgotten in last commit	letouzey	2008-03-19
*	migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...	letouzey	2008-03-19
*	Coq.Relations.Relations can move back to its short name	letouzey	2008-03-19
*	Do another pass on the typeclasses code. Correct globalization of class	msozeau	2008-03-19
*	tactique gappa	filliatr	2008-03-19
*	Various improvements of coqdep, resulting in a big speedup	letouzey	2008-03-19
*	Implementation of rewriting under lambdas. Tested on exists only.	msozeau	2008-03-18
*	Added a function to rebuild an elim scheme from elim_scheme_info. Will	courtieu	2008-03-18
*	Hint for Debian users.	glondu	2008-03-18
*	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
*	Correct implementation of normalization of signatures using setoid	msozeau	2008-03-18
*	* Small change in the make_eq_decidability call : the functions does not (yet)	vsiles	2008-03-18
*	Add the possibility of specifying constants to unfold for typeclass	msozeau	2008-03-17
*	* Factorizing code : context_chop was used in several files (even as chop_con...	vsiles	2008-03-17
*	Removed unneeded tactics from RelationClasses. Use	msozeau	2008-03-16