diff --git a/classical/unstable.v b/classical/unstable.v index e331d2836..8a82f1539 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -47,6 +47,20 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. +(* Backward compatibility with math-comp < 2.6, which has no [conjFieldType] + (the common ancestor of [rcfType] and [numClosedFieldType]). When it is + absent we alias it to [rcfType] via a global parsing-only abbreviation, so + that MCA files endowing [conjFieldType] with topological/normed structures + still compile: those instances then become redundant copies of the [rcfType] + ones (their [HB.no-new-instance] is silenced at each site). *) +Elpi Command analysis_declare_conjFieldType_compat. +Elpi Accumulate lp:{{ + main [] :- coq.locate-all "Num.ConjField.type" L, L = [_|_], !. + main [] :- @global! => coq.notation.add-abbreviation "conjFieldType" 0 + {{ Num.RealClosedField.type }} tt _. +}}. +Elpi analysis_declare_conjFieldType_compat. + Section IntervalNumDomain. Variable R : numDomainType. Implicit Types x : R. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 30e02866e..d0d20b781 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -221,6 +221,16 @@ HB.instance Definition _ := NormedModule.copy R R^o. HB.instance Definition _ := Num.ClosedField.on R. End numClosedFieldType. +Section conjFieldType. +Variable R : conjFieldType. +#[export, non_forgetful_inheritance, warnings="-HB.no-new-instance"] +HB.instance Definition _ := GRing.ComAlgebra.copy R R^o. +#[export, non_forgetful_inheritance, warnings="-HB.no-new-instance"] +HB.instance Definition _ := Vector.copy R R^o. +#[export, non_forgetful_inheritance, warnings="-HB.no-new-instance"] +HB.instance Definition _ := NormedModule.copy R R^o. +End conjFieldType. + Section numFieldType. Variable (R : numFieldType). #[export, non_forgetful_inheritance] diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index 9c90ac510..12985b65c 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -1,6 +1,8 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat all_algebra all_classical. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure pseudometric_structure. From mathcomp Require Import order_topology matrix_topology. @@ -130,6 +132,10 @@ HB.instance Definition _ (R : realFieldType) := PseudoPointedMetric.copy R R^o. HB.instance Definition _ (R : numClosedFieldType) := PseudoPointedMetric.copy R R^o. +#[export, non_forgetful_inheritance, warnings="-HB.no-new-instance"] +HB.instance Definition _ (R : conjFieldType) := + PseudoPointedMetric.copy R R^o. + #[export, non_forgetful_inheritance] HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.