coq/test-suite, 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 #14161: test-suite: add approve-coqdoc to update all coqdoc output files at once 2021-04-23T13:41:43+00:00 coqbot-app[bot] 2021-04-23T13:41:43+00:00 7e576aef5b41837c7faa72a5525ee41bec02babb Reviewed-by: SkySkimmer 
Reviewed-by: SkySkimmer
test-suite: add approve-coqdoc to update all coqdoc output files at once. 2021-04-23T13:00:57+00:00 Hugo Herbelin 2021-04-23T12:56:24+00:00 7e0c8172703111a026477cf704f50af9468f8f0a 






Enable canonical `fun _ => _` projections.
2021-04-22T07:16:22+00:00

Jan-Oliver Kaiser

2020-05-14T15:08:20+00:00

2cbc36c6ae4ca22e000dbb045c865f54a454aca3












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 #14131: Check for existence before using `Global.lookup_constant` instead of catching `Not_found`
2021-04-20T09:19:26+00:00

Pierre-Marie Pédrot

2021-04-20T09:19:26+00:00

cab7a5ddb906e5cef57d78ba7435e89354f3125b

Reviewed-by: ppedrot





Reviewed-by: ppedrot







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







Merge PR #14108: [zify] bugfix
2021-04-19T11:22:05+00:00

Vincent Laporte

2021-04-19T11:22:05+00:00

b53642ec813178fedd3e646832e7c033b8163f52

Reviewed-by: Zimmi48
Reviewed-by: vbgl





Reviewed-by: Zimmi48
Reviewed-by: vbgl







Check for existence before using `Global.lookup_constant` instead of catching `Not_found`
2021-04-19T10:46:13+00:00

Lasse Blaauwbroek

2021-04-19T09:08:03+00:00

e50a6195097c0d15c839c5403c1d02511afd54e4

`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.





`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.