Open maximedenes opened 4 years ago
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.
@maximedenes What is the status of this?
@maximedenes is this still relevant, or should we close it?
This is in preparation for https://github.com/coq/coq/pull/10734
Should be backward compatible