coq/test-suite/bugs, branch master The formal proof system 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 #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
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`.
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
[abbreviation] allow the user to set arguments scope 2021-04-07T17:59:46+00:00 Enrico Tassi 2021-03-19T13:29:07+00:00 d3963fc6b6dad5a0cf79815f31b2035ca8b3de25 






Merge PR #13741: Remove omega tactic (deprecated in 8.12)
2021-04-06T14:55:06+00:00

coqbot-app[bot]

2021-04-06T14:55:06+00:00

2360e5ba31c350f25d49fc71736282bfad9975ed

Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01





Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01







More extraction tests for inductive types with let-ins.
2021-04-04T18:20:01+00:00

Hugo Herbelin

2021-04-04T18:20:01+00:00

643c10a894c1db24dd8ab06cc4376c92ae8b7c3c












Fixing #13581: missing support for let-ins in arity of inductive types.
2021-04-04T09:01:25+00:00

Hugo Herbelin

2020-12-06T02:03:12+00:00

a265c1ad912b4940861ec27efd09e5b20d33233c

At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.





At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.