Adapt to https://github.com/math-comp/math-comp/pull/1545 (#154) #180
proux01Annotations
40 warnings
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L2980
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L488
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L237
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L191
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L189
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L187
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L174
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L172
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L154
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0):
finmap.v#L151
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L2980
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L488
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L237
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L191
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L189
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L187
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L174
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L172
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L154
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1):
finmap.v#L151
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L424
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L361
Use of "Notation" keyword for abbreviations is deprecated, use
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L237
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L191
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L189
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L187
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L174
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L172
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L154
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp-dev:rocq-prover-dev):
finmap.v#L151
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L2980
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L488
The '%' scope delimiter in 'Arguments' commands is deprecated, use
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L237
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L191
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L189
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L187
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L174
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L172
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L154
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
build (mathcomp/mathcomp-dev:rocq-prover-9.1):
finmap.v#L151
Postfix notations (i.e. starting with a nonterminal symbol and
|