coq - The formal proof system

Age	Commit message (Expand)	Author
2008-02-13	Suppression de l'option -glob-from de Coqdoc: les globalisations sont	notin
2008-02-13	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin
2008-02-13	Correction de ce qui semble être un petit bug dans la gestion de la	herbelin
2008-02-11	Correction d'un bug de clear	notin
2008-02-10	Fixing bug 1795 (occur check was not correctly done)	herbelin
2008-02-10	suppression code mort oublié lors du commit 10495	herbelin
2008-02-10	Granting wish 1794 (the name provided in the "using" clause of the	herbelin
2008-02-10	Backport Program Instance into Instance. Proper early error message if	msozeau
2008-02-10	Proposal of a nice notation for constructors xI and xO of type positive	letouzey
2008-02-10	Major revision: use of Function, including some non-structural ones	letouzey
2008-02-09	Major revision of FSetAVL: more Function, including some non-structural ones	letouzey
2008-02-09	Solde de code mort et petites optimisations sur lesquels je suis	herbelin
2008-02-09	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau
2008-02-08	misc improvements	letouzey
2008-02-08	Documentation of CHANGES and refman doc for the implicit argument binder	msozeau
2008-02-08	better comments in FMapInterface	letouzey
2008-02-08	better comments in FSetInterface	letouzey
2008-02-08	Change implementation of resolution for typeclasses to use a customized	msozeau
2008-02-08	Add more information to IllFormedRecBody exceptions, to show the exact	msozeau
2008-02-08	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau
2008-02-08	Add printer for Pp.std_ppcmds...	msozeau
2008-02-08	New "Preterm [ of id ] " command to show the preterm before giving it to	msozeau
2008-02-08	Backport code from command.ml to subtac_command.ml for definining	msozeau
2008-02-08	more complete FSets.v	letouzey
2008-02-08	updates concerning FSets	letouzey
2008-02-08	one forgotten compatibility lemma	letouzey
2008-02-08	Oubli dans r10524	notin
2008-02-08	Correction d'un bug de Coqdoc + ajout de Include dans les mots clés reconnus...	notin
2008-02-07	Mise en place d'une toute petite amélioration de l'unification de	herbelin
2008-02-06	Suite 10518	herbelin
2008-02-06	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin
2008-02-06	Détection plus souple et message un peu moins radical en cas de	herbelin
2008-02-06	Correction d'un bug à l'interprétation de "change" (on exigeait que	herbelin
2008-02-06	Résolution d'une confusion dans le rôle des variables CAMLP4 et CAMLP4LIB:	herbelin
2008-02-06	Fix obligations not being discharged due to new definition of complement.	msozeau
2008-02-06	New algorithm to resolve morphisms, after discussion with Nicolas	msozeau
2008-02-06	Work-in-progress to make eauto accept a list of goals as input and	msozeau
2008-02-06	Protection contre l'erreur mentionnée dans le rapport de bug 1790	herbelin
2008-02-05	kill some useless module aliases E:=X (for better name printing, see Elie's 1...	letouzey
2008-02-05	Correction d'un bug sur les substitutions:	soubiran
2008-02-05	Add Morphisms for Qceiling and Qfloor	roconnor
2008-02-05	Ajout d'un test pour le bug #1787	notin
2008-02-04	Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps	letouzey
2008-02-04	Instantiation of evars after instantiate (closes #1672).	glondu
2008-02-04	declaremods.ml	soubiran
2008-02-03	Add new files theories/Program/Basics.v and theories/Classes/Relations.v	msozeau
2008-02-02	fix the syntax "Include Type Foo"	letouzey
2008-02-02	factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...	letouzey
2008-02-01	Ajout de 2 tests	notin
2008-02-01	Thanks to Elie, we can share duplicated stuff in FSets: for a start, FSetWeak...	letouzey