coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
*	If a fixpoint is not written with an explicit { struct ... }, then	letouzey	2007-07-07
*	- Ajout de la possibilité d'utiliser la notation Record pour les	herbelin	2007-06-30
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Contrôle de la compatibilité de apply via une information dans les	herbelin	2007-05-28
*	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles	2007-05-25
*	Nettoyage et standardisation des messages d'erreurs.	herbelin	2007-05-17
*	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
*	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin	2007-04-29
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	Reorder hook and printing of message, more natural this way.	msozeau	2007-04-17
*	Added the option to set/unset the automatic generation of elimination schemes	vsiles	2007-04-17
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	Prévention notations récursives sans terminal à gauche et qui font boucler	herbelin	2007-03-15
*	bug#1434 importing fonctor arguments, now it works.	soubiran	2007-03-09
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin	2007-02-24
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
*	Vérification que toutes les evars ont étés instanciées dans les types imp...	herbelin	2007-02-07
*	Tentative amélioration messages d'erreur prédicat d'élimination (cf notamment	herbelin	2007-01-24
*	Merge from Lionel Elie Mamane's private branch:	lmamane	2007-01-10
*	Nouvelle approche pour le discharge modulaire	herbelin	2007-01-10
*	Cleaning backtracking code, optimized "Backtrack n x y" when n is	courtieu	2006-12-28
*	Addition of a "Combined Scheme" vernacular command for building the conjuncti...	msozeau	2006-12-23
*	Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...	notin	2006-12-12
*	Suite ajout option -output-context	herbelin	2006-12-08
*	Ajout d'une option -output-context qui affiche le contexte en CCI pur à la	herbelin	2006-12-08
*	Fixed the -emacs option which was always On.	courtieu	2006-11-24
*	Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de	herbelin	2006-11-21
*	The emacs-U option now does not output any char above 250.	courtieu	2006-11-17
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin	2006-10-28
*	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
*	Correction de la localisation des erreurs en interactif (numéro de	herbelin	2006-10-20
*	Amélioration de l'automatisation des coupures quand deux idents se suivent	herbelin	2006-10-09
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin	2006-10-05
*	Added a new option -emacs-U changing emacs prompt delimiters by	courtieu	2006-09-29
*	Corrections mineures	notin	2006-09-25
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	CompatibilitÃ© hyp=var dans Tactic Notation + nettoyage	herbelin	2006-09-15
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	Indentation + svnprop	notin	2006-09-12