| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-06-18 | Fix #12228 negative integers not accepted in ltac integer_list | Pierre Roux | |
| 2020-05-27 | Release notes for 8.12. | Théo Zimmermann | |
| 2020-05-17 | Ltac2: add notations for eval cbv in ... and other in place reductions | Michael Soegtrop | |
| 2020-05-12 | Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry. | Jason Gross | |
| Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: kyoDralliam | |||
| 2020-05-11 | Allow to rebind the old value of a mutable Ltac2 entry. | Pierre-Marie Pédrot | |
| 2020-05-08 | In non-strict mode, accept any variable as a tactic reference. | Pierre-Marie Pédrot | |
| Part of the plan of #11840. | |||
| 2020-05-02 | LtacProf now handles multi-success backtracking | Jason Gross | |
| Fixes #12196 | |||
| 2020-04-03 | Adding change log. | Hugo Herbelin | |
| 2020-03-08 | Minor improvements to the unreleased changelog. | Théo Zimmermann | |
| 2020-03-03 | Ltac2: Add notation for enough and eenough | Michael Soegtrop | |
| 2020-02-08 | Resolve #10342 : [Ltac2] Add array library | Michael Soegtrop | |
| 2020-01-22 | Changelog for 8.11.0. | Théo Zimmermann | |
| 2019-12-05 | Unfortunate bug with "cofix with": case of a CProdN over no bindings. | Hugo Herbelin | |
| Failing on CProdN([],...) was maybe a bit too radical. | |||
| 2019-12-02 | Move unreleased changelog to new 8.11 section. | Théo Zimmermann | |
| 2019-11-28 | [changelog] Add types to changelog entries. | Théo Zimmermann | |
| Types of changes are defined in the list defined by Keep a Changelog 1.0.0 (https://keepachangelog.com/en/1.0.0/): - Added - Changed - Deprecated - Fixed - Removed We exclude the type Security for now, even for soundness fixes, because the process of handling security vulnerabilities is different from anything we follow right now. | |||
| 2019-10-24 | Release notes for Coq 8.10.1 | Vincent Laporte | |
| 2019-10-21 | Adding changelog | Hugo Herbelin | |
| 2019-07-29 | Document changes by PR 10324 | Vincent Laporte | |
| White spaces are forbidden in the “&ident” syntax for ltac2 references. | |||
| 2019-06-08 | Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ↵ | Pierre-Marie Pédrot | |
| interpretation scopes Reviewed-by: Zimmi48 Reviewed-by: ppedrot Ack-by: vbgl | |||
| 2019-06-06 | [Ltac2] Interpretation scopes in “constr” arguments of tactic notations | Vincent Laporte | |
| 2019-06-05 | Changelog entry for Ltac2 (missing from #10002). | Théo Zimmermann | |
| 2019-05-05 | Create categories in changelog. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |