coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-16	Add change log for #12965.	Hugo Herbelin
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	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	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	Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbati...	Li-yao Xia
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	Merge PR #13368: Fix dune rules for @check-gram following recent changes.	coqbot-app[bot]
2020-11-15	Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve d...	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-15	Merge PR #13356: Make the universe of primitive arrays irrelevant	Pierre-Marie Pédrot
2020-11-14	Documenting one-line verbatim.	Hugo Herbelin
2020-11-14	Distinguish one_pattern and one_term nonterminals	Jim Fehrle
2020-11-14	Move destructuring let syntax closer to its documentation.	Théo Zimmermann
2020-11-14	Add changelog for #13376.	Hugo Herbelin
2020-11-13	Add changelog for #13373.	Hugo Herbelin
2020-11-13	Make the universe of primitive arrays irrelevant	Gaëtan Gilbert
2020-11-13	Fix dune rules for @check-gram following recent changes.	Théo Zimmermann
2020-11-13	Merge PR #12420: [stdlib] Decidable instance for negation	coqbot-app[bot]
2020-11-13	Add changelog for #13365	Li-yao Xia
2020-11-12	Add changelog entry for Proof using in -noinit mode.	Théo Zimmermann
2020-11-12	Move last changelog entry for 8.12.1.	Théo Zimmermann
2020-11-12	Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...	coqbot-app[bot]
2020-11-12	Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.	coqbot-app[bot]
2020-11-12	Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -I	coqbot-app[bot]
2020-11-12	Add documentation about the soundness bug.	Pierre-Marie Pédrot
2020-11-12	Add changelog for #13345.	Hugo Herbelin
2020-11-12	Clarifying the role of Add ML Path vs -I (see #13344).	Hugo Herbelin
2020-11-12	Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply	coqbot-app[bot]
2020-11-11	Add changelog for #13351.	Hugo Herbelin
2020-11-10	Merge PR #13315: Convert logic chapter to prodn	coqbot-app[bot]
2020-11-10	Convert logic.rst to prodn	Jim Fehrle
2020-11-10	Merge PR #13325: [compat] remove 8.10	coqbot-app[bot]
2020-11-09	Add additional escape sequences for notations	Jim Fehrle
2020-11-09	Add global version of OPTINREF	Jim Fehrle