coq - The formal proof system

Age	Commit message (Expand)	Author
2020-05-13	Documenting notations with both terms and binders.	Hugo Herbelin
2020-05-13	Merge section on Inductive types from Gallina and CIC.	Théo Zimmermann
2020-05-13	Create new file on Inductive types.	Théo Zimmermann
2020-05-13	Extract Inductive types from CIC.	Théo Zimmermann
2020-05-13	Merge sections on Inductive types and Recursive functions in new file.	Théo Zimmermann
2020-05-13	Add Recursive functions to new file on Inductive types.	Théo Zimmermann
2020-05-13	Extract Recursive functions from Gallina.	Théo Zimmermann
2020-05-13	Create new file on Inductive types.	Théo Zimmermann
2020-05-13	Extract Inductive types from Gallina.	Théo Zimmermann
2020-05-13	Merge sections on variants and match into new file.	Théo Zimmermann
2020-05-13	Merge sections on Variants and Private inductive types into new file.	Théo Zimmermann
2020-05-13	Add match to new file on Variants.	Théo Zimmermann
2020-05-13	Extract match from Gallina.	Théo Zimmermann
2020-05-13	Create a new file on Variants.	Théo Zimmermann
2020-05-13	Extract Variants from Gallina.	Théo Zimmermann
2020-05-13	Create a new file on Variants.	Théo Zimmermann
2020-05-13	Extract Private inductive types from Gallina.	Théo Zimmermann
2020-05-13	Create new file on sorts.	Théo Zimmermann
2020-05-13	Extract Sorts out of CIC.	Théo Zimmermann
2020-05-13	Added change log.	Hugo Herbelin
2020-05-13	Merge PR #12229: Hopefully consensual cleaning of keywords	Théo Zimmermann
2020-05-13	Merge PR #11828: [obligations] Deprecated flag cleanup	Gaëtan Gilbert
2020-05-13	Document the changes regarding the order of command-line options.	Théo Zimmermann
2020-05-12	Merge PR #12309: Remove documentation of -compile, which was removed in #8690.	Clément Pit-Claudel
2020-05-12	Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.	Jason Gross
2020-05-12	Merge PR #12223: Locating error again in atomic tactics (fixes #12152)	Pierre-Marie Pédrot
2020-05-12	Remove documentation of -compile, which was removed in #8690.	Théo Zimmermann
2020-05-12	Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le	Anton Trunov
2020-05-12	Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...	Pierre-Marie Pédrot
2020-05-12	documenting with examples the dynamic behaviour of Ltac2 Set	Kenji Maillard
2020-05-12	fuse changelogs for #11249 and #12237	Olivier Laurent
2020-05-11	Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.	Hugo Herbelin
2020-05-11	Checking validity of coqdoc file name.	Hugo Herbelin
2020-05-11	Correcting ltac2's documentation on values turning test into proper check.	Kenji Maillard
2020-05-11	Allow to rebind the old value of a mutable Ltac2 entry.	Pierre-Marie Pédrot
2020-05-11	Merge PR #12129: Add a `with_strategy` tactic	Pierre-Marie Pédrot
2020-05-10	Change log for #12223.	Hugo Herbelin
2020-05-10	Merge PR #12286: [sphinx] Add links to other versions of the refman	Théo Zimmermann
2020-05-09	[sphinx] Add links to other versions of the refman	Clément Pit-Claudel
2020-05-09	Merge PR #12241: [declare] Merge DeclareDef into Declare	Gaëtan Gilbert
2020-05-09	Revert "[with_strategy] Fix for coqchk"	Jason Gross
2020-05-09	[with_strategy] Work around #12191	Jason Gross
2020-05-09	Work around a bug in Coq in the doc	Jason Gross
2020-05-09	Elaborate with_strategy warning	Jason Gross
2020-05-09	Fix the `with_strategy` tactic to work with `abstract`	Jason Gross
2020-05-09	Add a `with_strategy` tactic	Jason Gross
2020-05-09	Hexadecimal: conversion to/from Coq strings	Pierre Roux
2020-05-09	Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections	Pierre Roux
2020-05-09	[doc] Add hexadecimal numerals	Pierre Roux
2020-05-09	Decimal: specify numeral notation for Q	Pierre Roux