coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Move definition of VO_TOOLS_DEP before first use of it.	lmamane	2007-01-17
*	Reintroduce compatibility with old versions of GNU make	lmamane	2007-01-17
*	Correction bug #1282	herbelin	2007-01-17
*	Correction bug #1302	herbelin	2007-01-17
*	Correction adresse CoRN dans FAQ (suite)	herbelin	2007-01-17
*	Correction adresse CoRN dans FAQ (cf #1317)	herbelin	2007-01-17
*	README update:	lmamane	2007-01-17
*	Various subtac fixes.	msozeau	2007-01-15
*	Suite au mail de Lionel a propos du Makefile:	letouzey	2007-01-12
*	un saut de ligne ...	letouzey	2007-01-12
*	addition du neq unicode	letouzey	2007-01-12
*	Petit oubli dans commit 9474	herbelin	2007-01-11
*	Ajout d'une option de débogage pour expliciter l'instance des evars	herbelin	2007-01-11
*	- Make .vo files depend on coqdoc if COQ_XML is set (bug #848)	lmamane	2007-01-10
*	Merge with Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Suite commit restructuration discharge (application du type de	herbelin	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Subtac fixes, support for reasoning on wf defs.	msozeau	2007-01-08
*	suite de la reparation du bug 1239: apres les inds, les records et vars de types	letouzey	2007-01-05
*	Rework subtac pattern matching equalities generation.	msozeau	2007-01-02
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
*	Protection contre une source possible de liaison de lambda anonyme	herbelin	2006-12-29
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	Correction petits bugs du check de la test-suite	herbelin	2006-12-28
*	Remplacement de la définition de Pind et Prec par une définition	herbelin	2006-12-28
*	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu	2006-12-28
*	Report correction bug #1289 dans trunk (r9435 pour branche v8.1)	herbelin	2006-12-26
*	Doc for Combined Scheme.	msozeau	2006-12-23
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	Default tactic for solving goals.	msozeau	2006-12-22
*	remplacement d'un test d'egalite par un test de convertibilite dans injection...	jforest	2006-12-22
*	typo malencontreuse	filliatr	2006-12-21