coq - The formal proof system

Age	Commit message (Expand)	Author
2018-10-05	[kernel] Remove section paths from `KerName.t`	Maxime Dénès
2018-09-11	Made names of existential variables interpretable as Ltac variables.	Hugo Herbelin
2018-09-10	Fixing ltac names interpretation in internals of pattern-matching compilation.	Hugo Herbelin
2018-09-10	Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.	Hugo Herbelin
2017-10-19	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann
2017-06-25	Reorganizing functions to find the relative position of an hypothesis.	Hugo Herbelin
2017-05-17	Merge PR#633: An extension of EXTEND and notations to make standard parsing t...	Maxime Dénès
2017-05-16	Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.	Hugo Herbelin
2017-05-01	Really fixing #2602 which was wrongly working because of #5487 hiding the cause.	Hugo Herbelin
2016-03-04	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot
2015-10-28	Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"	Hugo Herbelin
2015-10-18	Fixing #4198 (continued): not matching within the inner lambdas/let-ins	Hugo Herbelin
2015-10-11	Refining 0c320e79ba30 in fixing interpretation of constr under binders	Hugo Herbelin
2015-08-02	Continuing 817308ab (use ltac env for terms in ltac context) + fix	Hugo Herbelin
2015-08-02	Fixing #4221 (interpreting bound variables using ltac env was possibly	Hugo Herbelin
2014-09-15	Adapting ltac output test to new interpretation of binders.	Hugo Herbelin
2012-08-23	test-suite: Local Tactic Notation is now legal since r15731	letouzey
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-06-12	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot
2010-12-02	Fixing a bug introduced in r12304 (move of interpretation of	herbelin
2010-09-17	Fixed a problem introduced in r12607 after pattern_of_constr served	herbelin
2010-09-11	Improving a few error messages in Ltac interpretation	herbelin
2010-06-09	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-19	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras
2009-03-04	illegal tactic application was having Ltac interpreter loop	barras
2008-05-01	Clarification de l'ordre d'interprétation des variables dans ltac. En	herbelin
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2007-02-15	Réparation absence d'interprétation des liaisons vers listes	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2006-10-25	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin
2006-09-22	Test Tactic Notation	herbelin
2006-03-05	Ajout test relatif au bug #984	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2005-02-02	test de la bonne position des vars de ltac entre les vars et les rels	herbelin
2004-09-25	Ajouts	herbelin
2004-03-11	Ajout exemple Inst	herbelin
2003-05-22	Test backtracking	herbelin
2003-01-19	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin
2002-06-14	* empty log message *	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin
2002-06-13	Test de l'interprétation des fermetures de Match Context	herbelin
2001-12-21	* empty log message *	herbelin