coq - The formal proof system

Age	Commit message (Expand)	Author
2020-05-13	Create a new file on conversion.	Théo Zimmermann
2020-05-13	Extract conversion rules from CIC.	Théo Zimmermann
2020-05-13	Merge sections on CoInductive types and co-recursive functions in new file.	Théo Zimmermann
2020-05-13	Add cofix and CoFixpoint to file on CoInductive types.	Théo Zimmermann
2020-05-13	Extract cofix and CoFixpoint from Gallina.	Théo Zimmermann
2020-05-13	Create new file on CoInductive types.	Théo Zimmermann
2020-05-13	Extract CoInductive types from Gallina.	Théo Zimmermann
2020-05-13	Adding change log for #8808.	Hugo Herbelin
2020-05-13	Overlay elpi	Hugo Herbelin
2020-05-13	Documenting notations with both terms and binders.	Hugo Herbelin
2020-05-13	Extending support for mixing binders and terms in abbreviations.	Hugo Herbelin
2020-05-13	Tests for bugs #9583 (fixed by #11613) and #9679.	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	Merge PR #12293: Fix timestamp of coqchk manpage	Théo Zimmermann
2020-05-13	Make explicit that UGraph lower bounds are only of two kinds.	Pierre-Marie Pédrot
2020-05-13	do not re-export ListNotations from Program: kill overlays	Antonio Nikishaev
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	Centralize the OCaml version-checking function.	Pierre-Marie Pédrot
2020-05-13	Store the OCaml version used for Coq in vo files.	Pierre-Marie Pédrot
2020-05-13	Test interleaving of command-line options.	Théo Zimmermann
2020-05-13	Document the changes regarding the order of command-line options.	Théo Zimmermann
2020-05-13	Clarify the assignee's role in removing the overlay information	Anton Trunov
2020-05-13	Clarify the documentation for merging PRs with overlays	Anton Trunov
2020-05-12	Merge PR #12309: Remove documentation of -compile, which was removed in #8690.	Clément Pit-Claudel
2020-05-13	Merge PR #12307: Cleaning up the legacy proof engine	Emilio Jesus Gallego Arias
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	Merge PR #12190: [stdlib] [Permutation] Declare more instances as Global	Anton Trunov
2020-05-12	Remove a unused legacy tactic from Clenv.	Pierre-Marie Pédrot