coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	un warning pas beau supprimmé	filliatr	2001-04-23
*	Petit menage	delahaye	2001-04-20
*	* empty log message *	mayero	2001-04-19
*	Essais dans Ltac	delahaye	2001-04-19
*	Bug affichage d'implicites pour les vars liees	herbelin	2001-04-15
*	Non parenthesage des applications de tactiques	delahaye	2001-04-14
*	Ajout de _ dans les patterns d'intro	mohring	2001-04-12
*	Modified searchPattern. Before this correction, constructors were overlooked,	bertot	2001-04-10
*	Uniformisation des 'Save def_tok id'	herbelin	2001-04-09
*	nettoyage d'entrees de grammaires inutiles	courant	2001-04-09
*	branchement extraction en standard (pas de Require)	filliatr	2001-04-09
*	bug Print Proof; usage coqtop/coqc	filliatr	2001-04-06
*	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr	2001-04-05
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	Add a flag to avoid sending too many warnings when reloading syntax files	bertot	2001-04-04
*	adding entry points for the arguments of the Comment command.	bertot	2001-04-04
*	Adding A command for comments, this makes it possible to have structured	bertot	2001-04-04
*	The function filter_by_module, that was previously exported was not the	bertot	2001-04-03
*	Export a function (build_inductive) that is used in the graphical interface.	bertot	2001-04-03
*	branchement extraction (bytecode seulement)	filliatr	2001-03-30
*	amelioration de la structure des univers	barras	2001-03-28
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
*	Bug MUTCASE au lieu CASE	herbelin	2001-03-22
*	entetes	filliatr	2001-03-15
*	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin	2001-03-11
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	Bug affichage coercions	herbelin	2001-02-16
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Tentative d'amélioration affichage decls locales	herbelin	2001-02-16
*	Suppression sp_of_id	herbelin	2001-02-16
*	Prise en compte noms longs dans SuperAuto	herbelin	2001-02-16
*	Prise en compte noms longs dans Implicits	herbelin	2001-02-16
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14
*	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin	2001-02-14
*	Bug nommage Stdlib	herbelin	2001-02-13
*	Bug nombres en chiffres décimaux dans les Cases	herbelin	2001-02-12
*	Bug point final dans la syntaxe theorem_body	herbelin	2001-02-09
*	exported a few functions that are used in graphical interface pcoq.	bertot	2001-02-09
*	Several pairs of different functions actually had the same name, so	bertot	2001-02-09
*	modif de la syntax: assoc a droite pour Ring	mayero	2001-02-08
*	Simplifications	herbelin	2001-02-08
*	Modif pour les patterns de sous-termes	delahaye	2001-02-07
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin	2001-02-06
*	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin	2001-02-06
*	Extension coerce_to_var	herbelin	2001-02-05
*	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin	2001-02-05
*	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin	2001-02-05
*	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye	2001-02-05