Avoid relying on Add Field calling Add Ring.

[maximedenes]

This is in preparation for coq/coq#10734

Should be backward compatible

[spitters]

Ignored instance declaration for “in_mon_unit_zero”: “

∀ (K V : Type) (Ke : Equiv K) (Kplus : Plus K) (Kmult : Mult K)

(Kzero : Zero K) (Kone : One K) (Knegate : Negate K)

(Krecip : DecRecip K) (Ve : Equiv V) (Vop : SgOp V)

(Vunit : MonUnit V) (Vnegate : Negate V) (sm : ScalarMult K V)

(inp : Inproduct K V) (Kle : Le K),

InnerProductSpace K V → ∀ v : V, 0 = ⟨ v, v ⟩ ↔ v = mon_unit” is not a class

[not-a-class,typeclasses]

COQC theory/fields.v

File "./theory/fields.v", line 1, characters 0-112:

Warning: Notation "_ = _" was already used in scope type_scope.

[notation-overridden,parsing]

File "./theory/fields.v", line 1, characters 0-112:

Warning: Notation "_ ≠ _" was already used in scope type_scope.

[notation-overridden,parsing]

COQC theory/dec_fields.v

File "./theory/dec_fields.v", line 1, characters 0-199:

Warning: Notation "_ = _" was already used in scope type_scope.

[notation-overridden,parsing]

File "./theory/dec_fields.v", line 1, characters 0-199:

Warning: Notation "_ ≠ _" was already used in scope type_scope.

[notation-overridden,parsing]

File "./theory/dec_fields.v", line 209, characters 2-25:

Error: F2_ring_lemma1 already exists.

[maximedenes]

Ok, so this patch is in fact not backward compatible. I'll prepare an overlay in the Coq PR.

[Zimmi48]

I'll prepare an overlay in the Coq PR.

But there should be a backward compatible patch. Otherwise, it's not going to be possible to merge the PR, even after the Coq PR is merged.

[spitters]

@maximedenes What is the status of this?

[spitters]

@maximedenes is this still relevant, or should we close it?