Pierre Roux

Multiple scopes in Arguments and Bind Scope

4

The `Arguments` command only supported at most one scope for each argument. This PR enables multiple scopes. This would be useful for instance in MathComp where we'd like to bind...

Add parsing notations for _ = _ :> int and the like

5

##### Motivation for this change This way `2 = 1 :> int` is parsed as `2%Z = 1%Z` and not `2%R = 1%R` (that is `Posz 2 = Posz 1`...

Fix opp_fun_linear

2

##### Motivation for this change Fixes #916 ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries) - [ ] added corresponding documentation...

Initially reported on Zulip https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Cannot.20use.20existing.20linear.20structure.20of.20.60.5C-.20u.60 ```Coq From mathcomp Require Import all_ssreflect ssralg. Import GRing.Theory. Local Open Scope ring_scope. Section Test1. Context {R: ringType} (U V: lmodType R). Implicit Types (u...

To be merged in sync with the upstream PR

Uniformize semantics of :> in class after deprecation phase of #16230

17

This ends the deprecation phases of https://github.com/coq/coq/pull/16230 and https://github.com/coq/coq/pull/15802 that introduced :: instead of :> for subclasses in Class declarations. Now :> produces an error in `Class` before we can...

[stdlib] Warn about Vector.v

74

~Requires https://github.com/coq/coq/pull/18349 (merged)~ Following a few discussions on Zulip, it seems nice to warn new users about the fact that this part of the standard library is no longer state...

[Test] Put closed notations at level 0

2

Fixes / closes #???? - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new /...

To be merged in sync with the upstream PR.