coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-18	Support locality attributes for Hint Rewrite (including export)	Gaëtan Gilbert
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-14	Add checks for invalid occurrences in setoid rewrite.	Hugo Herbelin
2020-11-27	Revert "Remove deprecated tactic cutrewrite."	Théo Zimmermann
2020-11-20	Use nat_or_var where negative values don't make sense	Jim Fehrle
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
2020-09-08	Remove deprecated tactic cutrewrite.	Théo Zimmermann
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-06-26	[declare] Move proof information to declare.	Emilio Jesus Gallego Arias
2020-05-09	Add a `with_strategy` tactic	Jason Gross
2020-04-21	[declare] [tactics] Move declare to `vernac`	Emilio Jesus Gallego Arias
2020-04-15	[declare] Rename `Declare.t` to `Declare.Proof.t`	Emilio Jesus Gallego Arias
2020-04-15	[proof] Merge `Pfedit` into proofs.	Emilio Jesus Gallego Arias
2020-04-15	[proof] Merge `Proof_global` into `Declare`	Emilio Jesus Gallego Arias
2020-03-31	Try only using TC for conversion in cominductive (not great but let's see)	Gaëtan Gilbert
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-03	[exninfo] Deprecate aliases for exception re-raising.	Emilio Jesus Gallego Arias
2020-02-06	unsafe_type_of -> get_type_of in Extractactics.destauto_in	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> get_type_of in Extractactics.mkCaseEq	Gaëtan Gilbert
2019-11-30	Actually deprecate the `cutrewrite` tactic	Maxime Dénès
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-08-29	Make sure that all query commands return a notice (not an info) feedback	Maxime Dénès
2019-07-26	Remove unused grammar productions	Jim Fehrle
2019-06-24	[api] Remove `polymorphic` type alias, use labels instead.	Emilio Jesus Gallego Arias
2019-06-19	Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-16	Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".	Hugo Herbelin
2019-06-11	STM: encode in static types that vernac_when is only used when VtSideff	Gaëtan Gilbert
2019-06-09	[proof] Uniformize Proof_global API	Emilio Jesus Gallego Arias
2019-06-04	Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof	Gaëtan Gilbert
2019-06-04	coqpp: add new ![] specifiers for structured proof interaction	Gaëtan Gilbert
2019-06-04	Proof_global: pass only 1 pstate when we don't want the proof stack	Gaëtan Gilbert
2019-05-25	Documenting syntax "injection ... as [= pat1 ... patn ]".	Hugo Herbelin
2019-03-27	[geninterp] Track polymorphic status in tactic interpretation.	Emilio Jesus Gallego Arias
2019-03-27	[coqpp] [ltac] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-05	Make Program a regular attribute	Maxime Dénès
2018-12-12	Higher-level libobject API for objects with fixed scopes	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-19	Merge PR #9003: [vernacextend] Consolidate extension points API	Pierre-Marie Pédrot
2018-11-17	[vernacextend] Consolidate extension points API	Emilio Jesus Gallego Arias
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
2018-11-16	Remove the implicit tactic feature following #7229.	Pierre-Marie Pédrot
2018-11-05	Merge PR #8515: Command driven attributes	Pierre-Marie Pédrot
2018-11-02	coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax	Gaëtan Gilbert
2018-11-02	Command driven attributes.	Gaëtan Gilbert
2018-11-02	Move attributes out of vernacinterp to new attributes module	Gaëtan Gilbert
2018-10-30	Move abstract out of tactics.ml	Gaëtan Gilbert
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot