coq - The formal proof system

Age	Commit message (Expand)	Author
2008-04-01	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin
2008-04-01	Finish enhancemenent of return clause inference from tycons, integrating	msozeau
2008-04-01	Enhance handling of parameters in typeclass constraints: permit to specify an...	msozeau
2008-04-01	Add option to set the opacity of obligations to transparent, to be able	msozeau
2008-04-01	Correction du bug #1819	notin
2008-03-31	- Fix for rewriting under dependent products.	msozeau
2008-03-30	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-29	Fix test-suite files, change conflicting notation "->rel" and the others	msozeau
2008-03-28	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-27	- notations &&& and \|\|\| equivalent to andb and orb,	letouzey
2008-03-27	Various fixes on typeclasses:	msozeau
2008-03-26	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-25	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-24	Finish fix in command where we still lost information on what was a type	msozeau
2008-03-23	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-22	Compatibility fixes, backtrack on definitions of reflexive,	msozeau
2008-03-21	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-20	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-19	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-18	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