coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	HUGE COMMIT	sacerdot	2005-01-03
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...	herbelin	2004-12-29
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-25
*	Typo	herbelin	2004-12-24
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...	herbelin	2004-12-22
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Amélioration message localisation constructions et modules	herbelin	2004-12-09
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot	2004-12-07
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06