coq - The formal proof system

Age	Commit message (Expand)	Author
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
2008-03-18	* Small change in the make_eq_decidability call : the functions does not (yet)	vsiles
2008-03-17	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-16	Removed unneeded tactics from RelationClasses. Use	msozeau
2008-03-16	Using the "relation" constant made some unifications fail in the new	msozeau
2008-03-16	Ajout cible programs comme synonyme de subtac	herbelin
2008-03-16	Misc: Add test for bug 1704, now closed. Add usual syntax for lists in	msozeau
2008-03-16	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau
2008-03-16	Minor fixes on setoid rewriting. Now uses definitions of [relation] and	msozeau
2008-03-15	Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)	letouzey
2008-03-15	Forgot the test file.	msozeau
2008-03-15	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau
2008-03-15	Adapt funind to the RLetPattern constructor.	msozeau
2008-03-15	Backtrack sur le test censé discriminer entre une erreur d'evar non	herbelin
2008-03-15	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin
2008-03-14	Suppress some warnings by writing ugly Coq.Relations.Relations in some .v	letouzey
2008-03-14	avoid universe problems with pf_get_type in f_equal	letouzey
2008-03-14	New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefile	letouzey
2008-03-14	Backtrack wrong commit.	courtieu
2008-03-14	kill a warning (and clean the code around)	letouzey
2008-03-14	nettoyage de code obsolete.	soubiran
2008-03-14	Ajout des alias de module dans le noyau.	soubiran
2008-03-14	tactique gappa	filliatr
2008-03-14	indentation.	courtieu
2008-03-13	fix the 'decreasing on Xth' message	letouzey
2008-03-13	trying f	courtieu
2008-03-12	* Catching a Not_found exception when trying to use Scheme Equality	vsiles
2008-03-11	tactique Gappa : mise en place	filliatr
2008-03-11	Forget to update the CHANGES file after the commit r10180	vsiles
2008-03-11	tactique Gappa : mise en place	filliatr
2008-03-11	Typo commit 10653	herbelin
2008-03-10	Pas très propre de reposer sur la capture des anomalies (et cela	herbelin
2008-03-10	fold travaille maintenant sur la forme beta-iota-zeta réduite du	herbelin
2008-03-10	Indexation de pose proof, et par la même occasion du nouveau specialize	herbelin
2008-03-10	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin
2008-03-10	Fix compilation problem and finish little cleanup.	msozeau
2008-03-09	Add a missing morphism declaration that turns morphisms on R ==> R' to	msozeau
2008-03-09	Fix a few bugs in Program: use user-given typing constraints for	msozeau
2008-03-09	Des choses bizarres avec pa_op.cmo (extension syntaxique pour parser)	herbelin
2008-03-08	New implementation of Add Relation as a DefaultRelation instance	msozeau
2008-03-08	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest