coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Suppression de code mort	notin	2007-02-01
*	Report 9545 de 8.1 vers trunk	herbelin	2007-02-01
*	Petite relecture partie ring	herbelin	2007-02-01
*	Report de la révision 9577 dans le trunk	notin	2007-02-01
*	Abbreviation of order notation.	msozeau	2007-02-01
*	report de r9574: doc de field	barras	2007-01-31
*	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin	2007-01-31
*	MAJ ring	herbelin	2007-01-31
*	Correction typo eq_rec_eq (cf bug #1339)	herbelin	2007-01-31
*	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea	2007-01-31
*	Fix typo.	msozeau	2007-01-31
*	Fix order of wf and measure arguments, patch Program doc.	msozeau	2007-01-31
*	Nouvelle implantation de clear_hyps	notin	2007-01-30
*	suite du commit 9557	soubiran	2007-01-30
*	Petite correction sur un message d'erreur renvoyé au sous typage.	soubiran	2007-01-30
*	constr_of_pat bug with nested patterns.	msozeau	2007-01-30
*	bugfix for suffices (support for open head)	corbinea	2007-01-29
*	Various fixes in subtac, update some test cases.	msozeau	2007-01-29
*	finalized suffices	corbinea	2007-01-29
*	Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.	msozeau	2007-01-29
*	"suffices" implemented + syntax cleanup	corbinea	2007-01-28
*	Pas de solution à court terme pour ce problème de complexité	herbelin	2007-01-28
*	Explication du intros until n	notin	2007-01-26
*	Contounement d'un probleme avec la VM dans Function	jforest	2007-01-26
*	correction d'un bug d'efficacite dans le printer	jforest	2007-01-26
*	decl mode: anonymous facts	corbinea	2007-01-25
*	Redondance erronée dans les tests	herbelin	2007-01-25
*	doc de ring	bgregoir	2007-01-24
*	modifications des messages d'erreurs renvoyés lors de la comparaison	soubiran	2007-01-24
*	Update some tests and fix section bug.	msozeau	2007-01-24
*	changement de la fonction norm_subst	bgregoir	2007-01-24
*	Tentative amélioration messages d'erreur prédicat d'élimination (cf notamment	herbelin	2007-01-24
*	Correction bug #1333 (test non récursivité des dépendances en d'autres	herbelin	2007-01-24
*	Updated Makefile to include ConstructiveEpsilon.v	emakarov	2007-01-23
*	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov	2007-01-23
*	ring : Correction du bug PR#1306	bgregoir	2007-01-23
*	Correction du bug #1315:	notin	2007-01-22
*	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin	2007-01-22
*	Allègement de l'affichage des références par le printer si possible	herbelin	2007-01-22
*	Clarification redondance Axiome du choix unique/description	herbelin	2007-01-22
*	changes in declarative language : by term using tactic	corbinea	2007-01-22
*	Correction pour le rapport de bug #1325 par rétablissement du	herbelin	2007-01-22
*	Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent	herbelin	2007-01-22
*	Prise en compte des univers algébriques dans les types inférés dans	herbelin	2007-01-19
*	Export de l'afficheur de substitutions de noms de modules pour le débogueur	herbelin	2007-01-19
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Tests de référence circulaire au sous-typage de module (pour mémoire)	herbelin	2007-01-19
*	Update installation instructions to the modern world a bit.	lmamane	2007-01-18
*	Update for v8.1	lmamane	2007-01-18