From 2067f40d8cdda62c8044aad0cde020f6e77da158 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 12 Feb 2025 12:17:37 +0900 Subject: [PATCH 1/2] fixes #1464 --- theories/normedtype.v | 5 +++++ theories/topology_theory/num_topology.v | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 4ec2cd6271..17e44acf5b 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -18,6 +18,9 @@ From mathcomp Require Export real_interval separation_axioms tvs. (* $\mathbb{R}^n$ are the closed and bounded sets, Urysohn's lemma, Vitali's *) (* covering lemmas (finite case and infinite case), etc. *) (* *) +(* We endow `numFieldType` with the types of norm-related notions (accessible *) +(* with `Import numFieldNormedType.Exports). *) +(* *) (* * Limit superior and inferior: *) (* limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F *) (* f has type X -> \bar R. *) @@ -30,10 +33,12 @@ From mathcomp Require Export real_interval separation_axioms tvs. (* The HB class is PseudoMetricNormedZmod. *) (* ``` *) (* *) +(* ``` *) (* lower_semicontinuous f == the extented real-valued function f is *) (* lower-semicontinuous. The type of f is *) (* X -> \bar R with X : topologicalType and *) (* R : realType *) +(* ``` *) (* *) (* ## Normed modules *) (* ``` *) diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index c56d7512fe..a1bd6eb843 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -9,7 +9,7 @@ From mathcomp Require Import pseudometric_structure order_topology. (* # Topological notions for numerical types *) (* *) (* We endow `numFieldType` with the types of topological notions (accessible *) -(* with `Import numFieldTopology.Exports. *) +(* with `Import numFieldTopology.Exports). *) (* *) (******************************************************************************) From 0519f740450891a5b67aa9303336e00783ef3c3b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 12 Feb 2025 12:30:26 +0900 Subject: [PATCH 2/2] rm useless imports --- theories/convex.v | 1 - theories/realfun.v | 1 - 2 files changed, 2 deletions(-) diff --git a/theories/convex.v b/theories/convex.v index fbd28dd43d..5f87cd9a69 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -33,7 +33,6 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. diff --git a/theories/realfun.v b/theories/realfun.v index 865431d671..913489dab6 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -53,7 +53,6 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope.