coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Add the ability to specify what to do with free variables in instance	msozeau	2008-04-12
*	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau	2008-04-12
*	Check that no evars remain in instance types earlier at Instance	msozeau	2008-04-11
*	Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicit	msozeau	2008-04-09
*	Verify Setoid is loaded before doing anything.	msozeau	2008-04-09
*	Fixes in new Morphisms files.	msozeau	2008-04-09
*	Fix evar bugs in type classes:	msozeau	2008-04-09
*	contradict can now handle False hypothesis in the spirit of contradiction	letouzey	2008-04-09
*	Correction bug List.map2 dans Case12.v	herbelin	2008-04-09
*	Fix the last compilation problem	msozeau	2008-04-09
*	Fix compilation problem	msozeau	2008-04-09
*	correction of bug 1829	jforest	2008-04-08
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08
*	Ajout d'options a coqdoc pour l'entete html	notin	2008-04-08
*	Fix big de Bruijn bug in mutually recursive definitions.	msozeau	2008-04-07
*	Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :	herbelin	2008-04-06
*	Suite 10760	herbelin	2008-04-05
*	- Retour en arrière sur la capacité du nouvel apply à utiliser les	herbelin	2008-04-05
*	Minor fixes:	msozeau	2008-04-05
*	Mise en place d'une extension de apply pour que celui-ci sache	herbelin	2008-04-04
*	A file that can be loaded when a migration from Set to Type is desired	letouzey	2008-04-04
*	Correction problème de compil (blast.ml)	herbelin	2008-04-04
*	- Relâchement de la contrainte de bonne longueur des intropatterns	herbelin	2008-04-04
*	Test make 3.81	herbelin	2008-04-04
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand	herbelin	2008-04-04
*	- Amélioration de la présentation de RIneq, même si un nettoyage des	herbelin	2008-04-04
*	Protection de rewrite in contre le dépliage des constantes dans w_unify, ce qui	herbelin	2008-04-04
*	Essai d'un peu plus de conversion dans apply : suppression de la	herbelin	2008-04-03
*	New file FMapFullAVL containing the balancing proofs about FMapAVL:	letouzey	2008-04-03
*	Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ...	soubiran	2008-04-03
*	- Correction d'un bug de coq_makefile sur les variables CAMLLIBS et	notin	2008-04-03
*	Rework of FMapAVL inspired by recent changes of FSetAVL:	letouzey	2008-04-03
*	Chgts mineurs:	herbelin	2008-04-03
*	Patch sur le typage d'un foncteur applique a un alias.	soubiran	2008-04-03
*	Minor fixes. Use expanded type in class_tactics for Morphism search, to	msozeau	2008-04-02
*	Add the ability to specify the implicit status of section variables and	msozeau	2008-04-02
*	Typo affichage "simple apply"	herbelin	2008-04-01
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	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-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