coq - The formal proof system

Age	Commit message (Expand)	Author
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-04-11	Check that no evars remain in instance types earlier at Instance	msozeau
2008-04-09	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-08	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-07	Fix big de Bruijn bug in mutually recursive definitions.	msozeau
2008-04-06	Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :	herbelin
2008-04-05	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-04	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-03	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-02	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-01	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-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