coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-05	Add new page to writing proof index.	Théo Zimmermann
2020-11-05	Remove everything before term rewriting and simplification.	Théo Zimmermann
2020-11-05	Remove everything after term rewriting and simplification.	Théo Zimmermann
2020-11-05	Move some content to a new page on term rewriting and simplification.	Théo Zimmermann
2020-11-05	Merge PR #13231: Remove warning on SSR Search having moved.	coqbot-app[bot]
2020-11-05	Merge PR #13182: Check types when converting irrelevant terms in old unification	coqbot-app[bot]
2020-11-04	[stdlib] Decidable instance for negation	Yishuai Li
2020-11-05	Add overlays	Pierre Roux
2020-11-05	Add changelog	Pierre Roux
2020-11-05	Rename Dec and HexDec to Decimal and Hexadecimal	Pierre Roux
2020-11-05	[refman] Add an example for number notations	Pierre Roux
2020-11-05	Allow multiple primitive notation on the same scope and triggers	Pierre Roux
2020-11-05	[string notation] Handle parameterized inductives and non inductives	Pierre Roux
2020-11-05	Merge numeral and string notation plugins	Pierre Roux
2020-11-05	[numeral notation] Add support for parameterized inductives	Pierre Roux
2020-11-05	[numeral notation] Add tests for implicit arguments	Pierre Roux
2020-11-05	[numeral notation] Handle implicit arguments	Pierre Roux
2020-11-05	[numeral notation] Allow to put/ignore holes during pre/postprocessing	Pierre Roux
2020-11-05	[numeral notation] Prove R	Pierre Roux
2020-11-05	[numeral notation] Specify R	Pierre Roux
2020-11-05	[numeral notation] R	Pierre Roux
2020-11-05	[numeral notation] Prove Q	Pierre Roux
2020-11-05	[numeral notation] Specify Q	Pierre Roux
2020-11-05	[numeral notation] Q	Pierre Roux
2020-11-05	[numeral notation] Remove proofs for Q	Pierre Roux
2020-11-05	[numeral notation] Document the via ... using ... option	Pierre Roux
2020-11-04	[numeral notation] Add tests for the via ... using ... option	Pierre Roux
2020-11-04	Merge PR #13232: Adding an if-then-else syntax to Ltac2.	Michael Soegtrop
2020-11-04	[numeral notation] Adding the via ... using ... option	Pierre Roux
2020-11-04	[numeral notation] Add a pre/postprocessing	Pierre Roux
2020-11-04	Add functions Smartlocate.global_{constant,constructor}	Pierre Roux
2020-11-04	Add kernel/float64.ml to gitignore	Pierre Roux
2020-11-04	Regenerate the grammar description file.	Pierre-Marie Pédrot
2020-11-04	Document the syntax addition.	Pierre-Marie Pédrot
2020-11-04	Adding an if-then-else syntax to Ltac2.	Pierre-Marie Pédrot
2020-11-04	Adding change log for #13255.	Hugo Herbelin
2020-11-04	Typing patterns and using type constraints in Search.	Hugo Herbelin
2020-11-04	Adding a typed interpretation of patterns.	Hugo Herbelin
2020-11-04	Adding change log for #13301.	Hugo Herbelin
2020-11-04	Fixes #13298: primitive projections needs a correct typing environment.	Hugo Herbelin
2020-11-04	Merge PR #13193: [build] [native] Don't assume installed native libraries are...	coqbot-app[bot]
2020-11-04	Documentation of the main entry points of uState.mli.	Hugo Herbelin
2020-11-04	Factorizing UState.make* through UState.from_env, to highlight the similarity.	Hugo Herbelin
2020-11-04	Moving interpretation of user-level universes in constrintern.ml.	Hugo Herbelin
2020-11-04	Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.	Hugo Herbelin
2020-11-04	Merge PR #13258: Eagerly reduce rigid / flex conversion problems	coqbot-app[bot]
2020-11-04	Merge PR #13302: Fix test-suite in async mode.	coqbot-app[bot]
2020-11-04	Add overlays.	Pierre-Marie Pédrot
2020-11-04	Document the changes.	Pierre-Marie Pédrot
2020-11-04	Further code simplification in arbitrary hint interpretation.	Pierre-Marie Pédrot