math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
32 stars 2 forks source link

mathcomp2 and Sub deprecated #87

Closed thery closed 11 months ago

thery commented 1 year ago

I'm trying to use ring with mathcomp and I get a warning

From mathcomp Require Import all_ssreflect all_algebra ring.

Goal forall (T : fieldType) (x : T), x = x.
move=> T x.
ring.
Qed.
Warning: Notation sub is deprecated since mathcomp 2.0.0. Use Sub instead.
[deprecated-syntactic-definition-since-mathcomp-2.0.0,deprecated-since-mathcomp-2.0.0,deprecated-syntactic-definition,deprecated,default]
pi8027 commented 12 months ago

fresh emits a deprecation warning if the generated name is a deprecated name. I believe that this is a bug of Coq.

#[deprecated(since="1")] Notation a := id.

Goal False.
Proof.
let x := fresh "a" in
idtac.
(*
Warning: Notation a is deprecated since 1.
[deprecated-syntactic-definition-since-1,deprecated-since-1,deprecated-syntactic-definition,deprecated,default]
*)
Abort.
pi8027 commented 12 months ago

Reported: coq/coq#18133