coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Commentaire mort	herbelin	2005-12-28
*	Remplacement Pp.qs par Pptactic.qsnew	herbelin	2005-12-28
*	Autres suppressions de composantes du traducteur	herbelin	2005-12-27
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Petite correction nom QuantHypArgType suite suppression traducteur	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	Correction printer des Tactic Notation	herbelin	2005-12-23
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...	herbelin	2005-12-21
*	Changement des named_context	gregoire	2005-12-02
*	Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)	herbelin	2005-11-21
*	* empty log message *	barras	2005-11-18
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	- debugging og "Show Intros": no line breaking + fresh ids	coq	2005-11-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Niveau 99 permettant de parser { } nécessaire aussi dans l'entrée pattern	herbelin	2005-09-21
*	pas besoin de List.length pour savoir si une liste est vide	letouzey	2005-08-19
*	Add some debug printing functions.	coq	2005-07-15
*	Added entry constr_may_eval for tactic extensions (new syntax)	herbelin	2005-06-22
*	Ajout explicite du niveau 200 de pattern auquel on fait référence au niveau...	herbelin	2005-06-04
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Affinements suite à extension Tactic Notation aux tacticielles	herbelin	2005-05-17
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Globalisation des Tactic Notation	herbelin	2005-05-15
*	Allow auto to have a parametric argument (wish #967)	herbelin	2005-05-15
*	possibilité d'écrire [foo\| ] au lieu de [foo\|idtac]	letouzey	2005-05-09
*	Code v7 obsolete	herbelin	2005-05-05
*	Implementation of a new backtracking system, that allow to go back	coq	2005-04-20
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Keep ClosedSection marker for reset	herbelin	2005-02-20
*	Renaming Print Canonical Structure into Print Canonical Projections	herbelin	2005-02-18
*	Standardisation of function names about global references (especially, renami...	herbelin	2005-02-18
*	Bug affichage entiers négatifs	herbelin	2005-02-17
*	Nouvelle mouture Print Canonical Structures	herbelin	2005-02-12
*	Ajout Print Canonical Structures	herbelin	2005-02-12
*	Parseur pour la DTD XML de constr et un peu plus pour les arguments de tactiques	herbelin	2005-02-04
*	Ajout constructeur External pour appel outil externe à Coq	herbelin	2005-02-04
*	Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule (cu...	herbelin	2005-02-03
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Pour cible make doc	herbelin	2005-01-21
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Ajout de la syntaxe du reset label: "BackTo n".	coq	2005-01-14
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	Amélioration message Locate	herbelin	2005-01-13
*	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot	2005-01-13
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06