coq/user-contrib, branch master The formal proof system Merge PR #14158: Provide a reinit data for Ltac2 notations with entry level 4. 2021-04-23T15:57:15+00:00 coqbot-app[bot] 2021-04-23T15:57:15+00:00 528f8384dcd817e4e339719a5d99c30d48520a8e Reviewed-by: JasonGross 
Reviewed-by: JasonGross
Provide a reinit data for Ltac2 notations with entry level 4. 2021-04-23T07:08:45+00:00 Pierre-Marie Pédrot 2021-04-23T06:42:20+00:00 9b84b41009e5963b5ebb60938a921c5c16175d55 The grammar engine has the great idea to silently delete empty levels on rule removal. Since Ltac2 level 4 is initially empty, it means that when backtracking on the loading of the Ltac2 plugin, the grammar would be in a state where the level 4 was not there at all. There is a dedicated API for that situation in Pcoq, but it is kind of crazy that we have to use this kind of workaround when the problem is clearly that gramlib has the wrong default. Fixes #14156: Ltac2 broken with async. 
The grammar engine has the great idea to silently delete empty levels on rule
removal. Since Ltac2 level 4 is initially empty, it means that when backtracking
on the loading of the Ltac2 plugin, the grammar would be in a state where the
level 4 was not there at all.

There is a dedicated API for that situation in Pcoq, but it is kind of crazy
that we have to use this kind of workaround when the problem is clearly that
gramlib has the wrong default.

Fixes #14156: Ltac2 broken with async.
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
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 #14133: Slightly tweak the not-unit Ltac2 warning. 2021-04-20T20:55:51+00:00 coqbot-app[bot] 2021-04-20T20:55:51+00:00 3645c06030ed1266fd4160ec7211b4447731bf13 Reviewed-by: JasonGross 
Reviewed-by: JasonGross
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
Slightly tweak the not-unit Ltac2 warning. 2021-04-19T10:05:38+00:00 Pierre-Marie Pédrot 2021-04-19T10:05:38+00:00 9d3ea20fb8e9f1c3acfa3d127a1e3ee99fe7ebc9 Fixes #11683. 
Fixes #11683.
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