coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-20	Merge PR #13265: Add support for general non-necessarily-recursive binders in...	coqbot-app[bot]
2020-11-20	Merge PR #13352: Configure default value of -native-compiler	coqbot-app[bot]
2020-11-20	Add changelog for #13265.	Hugo Herbelin
2020-11-20	Add changelog	Pierre Roux
2020-11-20	Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...	coqbot-app[bot]
2020-11-20	Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clauses	Pierre-Marie Pédrot
2020-11-20	Merge PR #13403: Use only nats for occs_nums rather than ints	coqbot-app[bot]
2020-11-20	Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars...	Hugo Herbelin
2020-11-20	Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...	coqbot-app[bot]
2020-11-19	Adding changelog for #13237.	Hugo Herbelin
2020-11-19	[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.	Théo Zimmermann
2020-11-19	Add changelog for #13386.	Hugo Herbelin
2020-11-19	Merge PR #12984: [printing] Order notations by matching precision first, and ...	coqbot-app[bot]
2020-11-18	Use only nats for occs_nums rather than ints	Jim Fehrle
2020-11-18	Review commit: improving the doc of boolean attributes.	Théo Zimmermann
2020-11-18	[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.	Emilio Jesus Gallego Arias
2020-11-18	Adding change log for #12765.	Hugo Herbelin
2020-11-17	Adding change log for #12984.	Hugo Herbelin
2020-11-17	Add changelog for #12986.	Hugo Herbelin
2020-11-17	Merge PR #12653: Syntax for specifying cumulative inductives	coqbot-app[bot]
2020-11-16	Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0	coqbot-app[bot]
2020-11-16	Merge PR #13384: Warn on hints without an explicit locality	coqbot-app[bot]
2020-11-16	Add change log for #12965.	Hugo Herbelin
2020-11-16	[gc] Set GC policy as best-fit in OCaml >= 4.10.0	Emilio Jesus Gallego Arias
2020-11-16	Add changelog for #13337.	Hugo Herbelin
2020-11-16	Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...	coqbot-app[bot]
2020-11-16	Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` com...	Pierre-Marie Pédrot
2020-11-16	Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"	coqbot-app[bot]
2020-11-16	Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...	coqbot-app[bot]
2020-11-16	Merge PR #13188: Default disable automatic generalization of Instance type	Pierre-Marie Pédrot
2020-11-16	Merge PR #12685: Propagating scope information in indirect application to a r...	Pierre-Marie Pédrot
2020-11-16	Document the deprecation of the commands.	Pierre-Marie Pédrot
2020-11-16	Document the new warning.	Pierre-Marie Pédrot
2020-11-16	Merge PR #13388: Export locality for all hint commands	coqbot-app[bot]
2020-11-16	Merge PR #13365: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-free	coqbot-app[bot]
2020-11-16	Changelog for variance syntax	Gaëtan Gilbert
2020-11-16	Doc for variance syntax	Gaëtan Gilbert
2020-11-16	Merge PR #13290: Grant #13278: computation of return predicate takes care of ...	coqbot-app[bot]
2020-11-16	Slight improvement to the changelog entry.	Théo Zimmermann
2020-11-15	Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"	Jim Fehrle
2020-11-15	Add changelog for #13387.	Hugo Herbelin
2020-11-15	Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error...	coqbot-app[bot]
2020-11-15	Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...	coqbot-app[bot]
2020-11-15	Document the new export locality for the remaining hint commands.	Pierre-Marie Pédrot
2020-11-15	Add changelog for #13383.	Hugo Herbelin
2020-11-15	Doc and changelog for Instance Generalized Output	Gaëtan Gilbert
2020-11-15	Adding change log for #12685.	Hugo Herbelin
2020-11-15	Merge PR #13339: In -noinit mode, add support for Proof using, using is not a...	Pierre-Marie Pédrot
2020-11-14	Add changelog for #13376.	Hugo Herbelin
2020-11-13	Add changelog for #13373.	Hugo Herbelin