coq/doc/changelog, branch master The formal proof system Merge PR #14041: Enable canonical fun _ => _ projections. 2021-04-23T14:48:49+00:00 coqbot-app[bot] 2021-04-23T14:48:49+00:00 d332bbc3c1118631eb8c935ba61a8d071a90428e Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer 
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Merge PR #13965: [abbreviation] user syntax to set interp scope of argument 2021-04-23T14:33:27+00:00 Pierre-Marie Pédrot 2021-04-23T14:33:27+00:00 a0c3ebf4a6357a5140b98b4b40c71133c53d802e Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot 
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
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
Add changelog 2021-04-22T07:16:22+00:00 Pierre Roux 2021-04-02T12:07:39+00:00 82910bed2fccee7d1f4814e3339fbae374980e68 






Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.
2021-04-21T17:54:37+00:00

coqbot-app[bot]

2021-04-21T17:54:37+00:00

b8b8c73a4f62a8fb964e82c7c779a1aba3264bf4

Reviewed-by: JasonGross
Ack-by: jfehrle





Reviewed-by: JasonGross
Ack-by: jfehrle







Merge PR #13911: Remove the :> type cast?
2021-04-21T14:58:51+00:00

coqbot-app[bot]

2021-04-21T14:58:51+00:00

f9996cdaf0b6aee12c5b71432b1edb90dffb569a

Reviewed-by: mattam82
Ack-by: Zimmi48





Reviewed-by: mattam82
Ack-by: Zimmi48







Merge PR #14089: unify for Ltac2
2021-04-20T08:16:55+00:00

Pierre-Marie Pédrot

2021-04-20T08:16:55+00:00

b36fb9f68884090e5b06f9837da084395f519f96

Reviewed-by: ppedrot





Reviewed-by: ppedrot







changelog entry for Ltac2 unify
2021-04-19T18:24:50+00:00

Samuel Gruetter

2021-04-19T18:24:50+00:00

1dffce05d5b7b26a890a9d0359e54946e661511b












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.