coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	amelioration du pretty-print des modules	letouzey	2003-01-28
*	nouvelle gestion des constantes de type	letouzey	2003-01-28
*	all tactics should be covered now: remains	bertot	2003-01-26
*	Add translations for many tactics but a dozen are still remaining	bertot	2003-01-25
*	Inspect does not work for pcoq and there is no simple fix because inspect	bertot	2003-01-24
*	The data constructed when detecting an error in a list of commands must	bertot	2003-01-24
*	Corrects the way conjunctions, existential quantifications, and arrows are	bertot	2003-01-24
*	Make sure proof by pointing works.	bertot	2003-01-23
*	Make proof by pointing work for the new notations of existential quantification.	bertot	2003-01-23
*	oubli des add_recursors singleton logiques	letouzey	2003-01-23
*	maj V7.4	letouzey	2003-01-23
*	MAJ	herbelin	2003-01-22
*	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot	2003-01-22
*	petit bug pp haskell	letouzey	2003-01-22
*	Extraction des modules, enfin !	letouzey	2003-01-22
*	Make sure pcoq will also display hypotheses with a value.	bertot	2003-01-21
*	Add a few operators in the new version of xlate.ml and make sure	bertot	2003-01-21
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	Simplification de Simplify (plus de ())	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin	2003-01-15
*	Export M + Module M <: SIG	coq	2003-01-09
*	SearchAbout	filliatr	2003-01-06
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	Petit netoyage dans lib	coq	2002-12-19
*	suppression de l'archive cvs d'un bout de debug	letouzey	2002-12-19
*	les empty ind et les singletons etaient oublies par add_recursors	letouzey	2002-12-19
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	stupide inlining des construsteurs	letouzey	2002-12-18
*	Ajout "Locate Notation"	herbelin	2002-12-15
*	Evaluation paresseuse de l'affichage du debug	herbelin	2002-12-15
*	debut de parcours des modules	letouzey	2002-12-13
*	une branche de case inutile	letouzey	2002-12-13
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin	2002-12-10
*	Normalisation des types (fait avant dans Typing)	herbelin	2002-12-10
*	Ajoute le bon traitement pour Ring, Locate, Comments	bertot	2002-12-09
*	Take notations into account: numbers and the CNotation operator.	bertot	2002-12-09
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	pp	letouzey	2002-12-09
*	petit bug	letouzey	2002-12-09
*	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey	2002-12-09
*	reorganisation des recherches de ref dans ml_decl	letouzey	2002-12-05
*	code cleanup (+ debut de commencement de modules)	letouzey	2002-12-05
*	Modification Require From	mohring	2002-12-04
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
*	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot	2002-12-03