From ebb43c8a34bb9e9aeb48e8535501e76afcbe9da5 Mon Sep 17 00:00:00 2001 From: Guillaume Baudart Date: Fri, 5 Jun 2026 15:41:57 +0900 Subject: [PATCH] To preserve the mathcomp CI (forward dependency) for PR#1611 Developed with the assistance of Claude Opus 4.8 (1M context). Co-authored-by: Cyril Cohen Co-authored-by: Reynald Affeldt --- classical/unstable.v | 14 ++++++++++++++ theories/normedtype_theory/normed_module.v | 10 ++++++++++ theories/topology_theory/num_topology.v | 6 ++++++ 3 files changed, 30 insertions(+) diff --git a/classical/unstable.v b/classical/unstable.v index e331d2836d..8a82f15394 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 30e02866ea..d0d20b7814 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 9c90ac5101..12985b65cc 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.