coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* empty log message *	barras	2003-03-12
*	Remove a TODO in the translation of generic arguments:	bertot	2003-03-10
*	Make sure that identifiers are parsed as qualified identifier and that	bertot	2003-03-06
*	Ajout du traducteur	desmettr	2003-02-05
*	Added a clause for VernacDefineModule, but with an error as result.	bertot	2003-02-03
*	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
*	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot	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
*	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
*	SearchAbout	filliatr	2003-01-06
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	Ajout "Locate Notation"	herbelin	2002-12-15
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Ajout options -v7 et -v8, et commandes V7only et V8only	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
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	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
*	Raffinement syntaxe Infix	herbelin	2002-11-29
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24
*	Complétion du commit précédent	herbelin	2002-11-16
*	Passage à une représentation des fixpoints plus primitive dans constr_expr ...	herbelin	2002-11-15
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-28
*	Clarification changements autour de Remark/Fact/Local	herbelin	2002-10-23
*	TacCall attend une référence	herbelin	2002-10-14
*	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin	2002-10-14
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	Lazy manuelles dans le code	coq	2002-10-07
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Re-introduce the treatement of Tacticals that Hugo had already done in	bertot	2002-10-04
*	Previous version did compile but did not make it possible to actually run	bertot	2002-10-03
*	Complétion filtrage	herbelin	2002-09-29
*	Un peu (plus) d'ordre dans Nametab...	coq	2002-09-24
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03