coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-12-09	Amélioration message localisation constructions et modules	herbelin
2004-12-07	* added subst_evaluable_reference	sacerdot
2004-12-07	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot
2004-12-06	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-11-27	Indépendance vis à vis de Symbols (suite)	herbelin
2004-11-22	Bug commit 1.71	herbelin
2004-11-22	Correction bug Notation: il faut re-déclarer les règles de parsing des nota...	herbelin
2004-11-22	compatibility with POWERPC	gregoire
2004-11-20	'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marche	herbelin