coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-23	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-02	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot
2015-12-22	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond
2015-12-18	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik
2015-12-18	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik
2015-12-18	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik
2015-12-18	Tying the loop in tactic printing API.	Pierre-Marie Pédrot
2015-11-02	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin
2015-10-08	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot
2015-10-08	Goptions: new value type: optional string	Enrico Tassi
2015-09-14	Univs: Add universe binding lists to definitions	Matthieu Sozeau
2015-08-14	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross
2015-06-26	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg
2015-05-04	Add a [Redirect] vernacular command	Clément Pit--Claudel
2015-04-23	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond
2015-03-27	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot
2015-02-14	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi
2015-01-12	Update headers.	Maxime Dénès
2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi
2014-12-15	About now accepts hypothesis names and goal selector.	Pierre Courtieu
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-11-10	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot
2014-11-05	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas
2014-11-05	printing/Ppvernac: Fix missing keyword tagging on theorem introducers.	Yann Régis-Gianas
2014-11-05	printing/Ppvernac: Fix missing keyword tagging on definition introducers.	Yann Régis-Gianas
2014-11-05	printing/Ppvernac: Cosmetics.	Yann Régis-Gianas
2014-11-04	printing/Ppannotation: New annotation for tactic syntactic objects.	Regis-Gianas
2014-11-04	Rebase artefact.	Regis-Gianas
2014-11-04	lib/Pp.tag: New.	Regis-Gianas
2014-11-04	printing/Ppannotation: Introduce a new annotation for keywords.	Regis-Gianas
2014-11-04	Ppannotation.t: New constructor AVernac.	Regis-Gianas
2014-11-04	Ppvernac.Make: New	Regis-Gianas
2014-11-04	Ppvernac: Cosmetics.	Regis-Gianas
2014-11-01	Add [Info] command.	Arnaud Spiwack
2014-10-13	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi
2014-09-30	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin
2014-09-29	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi
2014-09-25	Improve consistency of whitespace (beautifier).	Xavier Clerc
2014-09-15	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau
2014-09-12	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2014-09-04	Remove [Infer] option of records.	Arnaud Spiwack
2014-09-04	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack
2014-08-21	Improve consistency of whitespace (beautifier).	Xavier Clerc
2014-08-21	Improve consistency of whitespace (beautifier).	Xavier Clerc
2014-08-21	Space after [identity] coercion keywords (beautifier).	Xavier Clerc
2014-08-21	Avoid redundant spaces (beautifier).	Xavier Clerc
2014-08-21	Do not drop the locality qualifier (beautifier).	Xavier Clerc