coq - The formal proof system

Age	Commit message (Expand)	Author
2001-05-03	Changement de la structure des points fixes	barras
2001-04-25	message d'erreur pour rattrapper l'anomalie avec SQUASH	barras
2001-04-25	Amelioration affichage	herbelin
2001-04-24	Messages d'erreur Cases	herbelin
2001-04-24	Les clauses de Rec doivent prendre des tactic_atom's	delahaye
2001-04-23	un warning pas beau supprimmé	filliatr
2001-04-20	Petit menage	delahaye
2001-04-19	* empty log message *	mayero
2001-04-19	Essais dans Ltac	delahaye
2001-04-15	Bug affichage d'implicites pour les vars liees	herbelin
2001-04-14	Non parenthesage des applications de tactiques	delahaye
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-10	Modified searchPattern. Before this correction, constructors were overlooked,	bertot
2001-04-09	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-06	bug Print Proof; usage coqtop/coqc	filliatr
2001-04-05	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr
2001-04-04	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-03	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-03-30	branchement extraction (bytecode seulement)	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-22	Bug MUTCASE au lieu CASE	herbelin
2001-03-15	entetes	filliatr
2001-03-11	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-02-16	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-14	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-13	Bug nommage Stdlib	herbelin
2001-02-12	Bug nombres en chiffres décimaux dans les Cases	herbelin
2001-02-09	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-08	modif de la syntax: assoc a droite pour Ring	mayero
2001-02-08	Simplifications	herbelin
2001-02-07	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-06	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin