coq-community
Avoid relying on `Add Field` calling `Add Ring`.
This is in preparation for https://github.com/coq/coq/pull/10734
Should be backward compatible
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.
Ok, so this patch is in fact not backward compatible. I'll prepare an overlay in the Coq PR.
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.
