coq - The formal proof system

Age	Commit message (Expand)	Author
2005-12-21	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-02	Changement des named_context	gregoire
2005-11-21	Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)	herbelin
2005-11-18	* empty log message *	barras
2005-11-08	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-02	Types inductifs parametriques	mohring
2005-09-21	Niveau 99 permettant de parser { } nécessaire aussi dans l'entrée pattern	herbelin
2005-08-19	pas besoin de List.length pour savoir si une liste est vide	letouzey
2005-07-15	Add some debug printing functions.	coq
2005-06-22	Added entry constr_may_eval for tactic extensions (new syntax)	herbelin
2005-06-04	Ajout explicite du niveau 200 de pattern auquel on fait référence au niveau...	herbelin
2005-05-20	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-17	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-15	Globalisation des Tactic Notation	herbelin
2005-05-15	Allow auto to have a parametric argument (wish #967)	herbelin
2005-05-09	possibilité d'écrire [foo\| ] au lieu de [foo\|idtac]	letouzey
2005-05-05	Code v7 obsolete	herbelin
2005-04-20	Implementation of a new backtracking system, that allow to go back	coq
2005-03-07	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-02-20	Keep ClosedSection marker for reset	herbelin
2005-02-18	Renaming Print Canonical Structure into Print Canonical Projections	herbelin
2005-02-18	Standardisation of function names about global references (especially, renami...	herbelin
2005-02-17	Bug affichage entiers négatifs	herbelin
2005-02-12	Nouvelle mouture Print Canonical Structures	herbelin
2005-02-12	Ajout Print Canonical Structures	herbelin
2005-02-04	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-03	Clarification des niveaux pr_constr et pr_lconstr en v8 dans pr_prim_rule (cu...	herbelin
2005-01-21	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-14	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-13	Amélioration message Locate	herbelin
2005-01-13	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot
2005-01-06	- Module/Declare Module syntax made more uniform:	sacerdot
2005-01-03	HUGE COMMIT	sacerdot
2005-01-02	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin
2004-12-29	ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...	herbelin
2004-12-25	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-12-24	Typo	herbelin
2004-12-24	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-12-22	Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...	herbelin
2004-12-09	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin