coq - The formal proof system

Age	Commit message (Expand)	Author
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-03-21	+ destruct now works as induction on multiple arguments :	jforest
2006-03-17	Modification des propriétés (svn:executable)	notin
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-01-28	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2006-01-28	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin
2006-01-24	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin
2006-01-21	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin
2006-01-16	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin
2006-01-11	remove warnings that were left in the directory contrib/interface	bertot
2006-01-11	removes several warnings in contrib/interface	bertot
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-30	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Achèvement suppression traducteur dans contrib/interface	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-23	Simplifification de vernac_expr li l'abandon du traducteur	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-14	adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,	bertot
2005-11-02	Types inductifs parametriques	mohring
2005-05-20	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot
2005-05-19	added VernacBacktrack (new backtracking command dedicated to	coq
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-05-15	Allow auto to have a parametric argument (wish #967)	herbelin
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	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-12	Ajout Print Canonical Structures	herbelin
2005-02-06	Nettoyage et documentation de Library	herbelin
2005-01-26	Ajout cas VernacBackTo	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
2004-12-24	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-12-09	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin
2004-12-07	* added subst_evaluable_reference	sacerdot
2004-12-06	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin
2004-11-29	Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...	herbelin
2004-11-29	Commit précédent erroné; retour version précédente	herbelin
2004-11-28	MAJ vis à vis de extratactics	herbelin
2004-11-17	Locate Module	herbelin
2004-11-17	New command "Print Rewrite HindDb dbname".	sacerdot
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot