coq/doc/sphinx/proof-engine, branch master

Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.

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

Reviewed-by: JasonGross
Ack-by: jfehrle

Merge PR #13815: Improve description of conversions

2021-04-19T09:14:24+00:00

Reviewed-by: Zimmi48
Ack-by: JasonGross

Disambiguate move tactics.

2021-04-17T17:17:38+00:00

Properly pass the Ltac2 notation level to the gramlib API.

2021-04-16T22:10:03+00:00

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

Reviewed-by: JasonGross

Remove the omega tactic and related options

2021-04-03T01:52:59+00:00

Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations

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

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

Documenting the changes.

2021-03-13T13:44:51+00:00

Add documentation.

2021-03-10T11:23:41+00:00

Regenerate the Ltac2 syntax for documentation.

2021-03-10T11:20:27+00:00