coq/test-suite/output, branch master

Merge PR #14041: Enable canonical fun _ => _ projections.

2021-04-23T14:48:49+00:00

Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer

Enable canonical `fun _ => _` projections.

2021-04-22T07:16:22+00:00

[abbreviation] allow the user to set arguments scope

2021-04-07T17:59:46+00:00

Merge PR #14035: Fix printing of ssr do intros and seq tactics

2021-03-31T15:48:13+00:00

Reviewed-by: gares
Reviewed-by: ppedrot

Fix printing of ssr do intros and seq tactics

2021-03-31T12:20:08+00:00

Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to check for conversion

2021-03-25T18:40:29+00:00

Reviewed-by: gares
Ack-by: SkySkimmer

Merge PR #13852: [vernac] Improve alpha-renaming in record projection types

2021-03-25T16:24:37+00:00

Reviewed-by: SkySkimmer

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

Minimize the set of multiple inheritance paths to check for conversion

2021-03-12T17:09:53+00:00

The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of a pair of multiple inheritance
paths (of coercions) will be skipped if these paths can be reduced to smaller
adjoining pairs of multiple inheritance paths, and this reduction will be
determined based on that reachability information.

Merge PR #13840: [notation] option to fine tune printing of literals

2021-03-10T13:53:55+00:00

Reviewed-by: SkySkimmer
Ack-by: jfehrle