coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	refined the conversion oracle	barras	2008-05-21
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	Correction bug #1842 + correction bug initialisation introduit dans	herbelin	2008-05-10
*	Efficacité, bugs, robustesse CoqIDE	herbelin	2008-05-08
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	- Add "Global" modifier for instances inside sections with the usual	msozeau	2008-04-15
*	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau	2008-04-12
*	- Retour en arrière sur la capacité du nouvel apply à utiliser les	herbelin	2008-04-05
*	Add the ability to specify the implicit status of section variables and	msozeau	2008-04-02
*	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau	2008-03-23
*	Do another pass on the typeclasses code. Correct globalization of class	msozeau	2008-03-19
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Change notation for setoid inequality, coerce objects before comparing them. ...	msozeau	2008-01-18
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Print Assumptions est pret pour la release.	aspiwack	2007-12-17
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Nettoyage de Print Assumptions :	aspiwack	2007-11-09
*	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin	2007-11-08
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	bug#1434 importing fonctor arguments, now it works.	soubiran	2007-03-09
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin	2006-11-21
*	Ajout option Set Printing Universes et amélioration affichage des univers	herbelin	2006-10-28
*	bug #1194: normalisation evars a la sortie de focus	barras	2006-10-23
*	Add a flush after backtracking x y z and before printing subgoals.	courtieu	2006-10-23
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Indentation + typo	notin	2006-09-01
*	Correction du bug #1116	jforest	2006-07-20
*	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin	2006-07-05
*	Modification of emacs output: No more show script at the end of a proof.	courtieu	2006-04-27
*	Modification of "Show Intros": it now shows letins too.	courtieu	2006-04-11
*	Suppression du test Proof with <tac>	notin	2006-04-05
*	- correction du bug #1055	notin	2006-03-27
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	* empty log message *	coq	2006-01-16
*	Correction dans vernac_exact_proof -- jmn	coq	2006-01-16
*	Correction du bug #1055	coq	2006-01-13
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26