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
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	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
*	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
*	Renaming Print Canonical Structure into Print Canonical Projections	herbelin	2005-02-18
*	Ajout Print Canonical Structures	herbelin	2005-02-12
*	Ajout constructeur External pour appel outil externe à Coq	herbelin	2005-02-04
*	Ajout constructeur External pour appel outil externe à Coq	herbelin	2005-02-04
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Ajout de la syntaxe du reset label: "BackTo n".	coq	2005-01-14
*	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot	2005-01-13
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06
*	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-24
*	pp of nested fixpoints (dangling with/for)	barras	2004-12-01
*	Export pr_intro_pattern	herbelin	2004-11-30
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	Ajout 'Locate Module'	herbelin	2004-11-17
*	Affichage des univers	herbelin	2004-11-04
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...	herbelin	2004-10-12
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	"Print Setoids" command added.	sacerdot	2004-07-23
*	Abstraction vis à vis du type loc pour compatibilité ocaml 3.08	herbelin	2004-07-16
*	Nouvelle en-tête	herbelin	2004-07-16
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	more evar stuff	corbinea	2004-06-28
*	Plus de robustesse en traduisant les 'Repeat Induction' et les 'Do n Induction'	herbelin	2004-06-02
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
*	Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...	herbelin	2004-04-08
*	code mort	herbelin	2004-03-24
*	Traduction ad hoc pour Hint Rewrite in using	herbelin	2004-03-18
*	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin	2004-03-17
*	Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...	herbelin	2004-03-17
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	Bug inversion abstract_constr_expr et prod_constr_expr	herbelin	2004-03-12
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur la...	herbelin	2004-03-05
*	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin	2004-03-03
*	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin	2004-03-02
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin	2004-03-02
*	Généralisation du type ltac Identifier en IntroPattern; prise en compte des...	herbelin	2004-03-01
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26