coq/doc/changelog/05-tactic-language, branch master The formal proof system Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function. 2021-04-22T11:55:14+00:00 coqbot-app[bot] 2021-04-22T11:55:14+00:00 d758cc5bb19d7abfcce13d2c26b5ae1c0fc1a439 Reviewed-by: JasonGross 
Reviewed-by: JasonGross
Uniformize the name of the Ltac2 boolean equality function. 2021-04-17T18:11:06+00:00 Pierre-Marie Pédrot 2021-04-17T18:08:36+00:00 e27fdd18cdfd8424d19058a3b59256219d111733 All other equality functions are called "equal" but this one was called "eq". We add a deprecated alias for backward compatibility. 
All other equality functions are called "equal" but this one was called "eq".
We add a deprecated alias for backward compatibility.
Properly pass the Ltac2 notation level to the gramlib API. 2021-04-16T22:10:03+00:00 Pierre-Marie Pédrot 2021-04-08T13:39:56+00:00 f6e393dae62afbb659eab64a530c0cf39403c495 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. 
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.
Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation. 2021-04-16T15:54:04+00:00 coqbot-app[bot] 2021-04-16T15:54:04+00:00 f337187f0ac4c2062031225234fd23b436b979b5 Reviewed-by: JasonGross 
Reviewed-by: JasonGross
Added a changelog. 2021-03-29T08:35:59+00:00 Pierre-Marie Pédrot 2021-03-29T08:35:59+00:00 529243826c3a51ca0bc6d37cf0f1d3c697b8a3e9 






Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations
2021-03-23T20:55:59+00:00

Michael Soegtrop

2021-03-23T20:55:59+00:00

47c20236f578dca9381822a62b5a406d6b42676d

Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle





Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle







Merge PR #13914: Allow the presence of type casts for return values in Ltac2.
2021-03-23T20:52:04+00:00

Michael Soegtrop

2021-03-23T20:52:04+00:00

fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88

Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48





Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48







Adding a changelog and registering the new file in the documentation.
2021-03-16T19:02:56+00:00

Pierre-Marie Pédrot

2021-03-10T13:07:46+00:00

761d3ccaf6a593a73811da38fa731c2f601902f8












Documenting the changes.
2021-03-13T13:44:51+00:00

Pierre-Marie Pédrot

2021-03-13T13:42:36+00:00

650461653aa1d4bc47509f0a2c49c3a235fb6381












Add documentation.
2021-03-10T11:23:41+00:00

Pierre-Marie Pédrot

2021-01-21T15:54:19+00:00

234a802f0925f9c9078417afa28dcb00c31668d9