| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-22 | Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function. | coqbot-app[bot] | |
| Reviewed-by: JasonGross | |||
| 2021-04-17 | Uniformize the name of the Ltac2 boolean equality function. | Pierre-Marie Pédrot | |
| All other equality functions are called "equal" but this one was called "eq". We add a deprecated alias for backward compatibility. | |||
| 2021-04-17 | Properly pass the Ltac2 notation level to the gramlib API. | Pierre-Marie Pédrot | |
| For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence. | |||
| 2021-04-16 | Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation. | coqbot-app[bot] | |
| Reviewed-by: JasonGross | |||
| 2021-03-29 | Added a changelog. | Pierre-Marie Pédrot | |
| 2021-03-23 | Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵ | Michael Soegtrop | |
| notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle | |||
| 2021-03-23 | Merge PR #13914: Allow the presence of type casts for return values in Ltac2. | Michael Soegtrop | |
| Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48 | |||
| 2021-03-16 | Adding a changelog and registering the new file in the documentation. | Pierre-Marie Pédrot | |
| 2021-03-13 | Documenting the changes. | Pierre-Marie Pédrot | |
| 2021-03-10 | Add documentation. | Pierre-Marie Pédrot | |
| 2021-03-10 | Adding documentation of the changes. | Pierre-Marie Pédrot | |
| 2021-01-22 | Add documentation for Ltac2 Printf. | Pierre-Marie Pédrot | |
| 2020-12-04 | Merge PR #13442: Add an abstraction function in the LtacX FFI. | coqbot-app[bot] | |
| Reviewed-by: kyoDralliam | |||
| 2020-12-03 | [changelog] update markup | Enrico Tassi | |
| 2020-12-03 | Changes for Coq 8.13 | Matthieu Sozeau | |
| 2020-11-30 | Adding a changelog for Ltac1.lambda. | Pierre-Marie Pédrot | |
| 2020-11-05 | Changelog for 8.12.1. | Théo Zimmermann | |
| 2020-11-04 | Document the syntax addition. | Pierre-Marie Pédrot | |
| 2020-10-28 | Adding changelog for #13247. | Hugo Herbelin | |
| 2020-09-22 | Adding change log for #13028. | Hugo Herbelin | |
| 2020-07-23 | [changelog] Latest changes backported to 8.12 branch. | Emilio Jesus Gallego Arias | |
| 2020-07-01 | Add a changelog. | Pierre-Marie Pédrot | |
| 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 |