correct imports

UOR-Foundation · Feb 17, 2025 · 5d0d2b0 · 5d0d2b0
1 parent 06197b1
commit 5d0d2b0
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 6 deletions.
diff --git a/coq/CompactResolvent.v b/coq/CompactResolvent.v
@@ -6,7 +6,7 @@
 Require Import Reals.
 Require Import Coquelicot.Coquelicot.
 Require Import Psatz.
-Require Import MyUOR_H1.
+Require Import UOR_H1_HPO.
 Open Scope R_scope.
 
 (* We assume that the domain D_H1 of H1 is a Sobolev space (e.g., H¹₀ ∩ H²) and that the

diff --git a/coq/Eigenfunctions.v b/coq/Eigenfunctions.v
@@ -7,7 +7,7 @@
 Require Import Reals.
 Require Import Coquelicot.Coquelicot.
 Require Import Psatz.
-Require Import MyUOR_H1.
+Require Import UOR_H1_HPO.
 Open Scope R_scope.
 
 (* We assume by axiom that for each n, ψ n satisfies the eigenvalue equation:

diff --git a/coq/InverseSpectralTheory.v b/coq/InverseSpectralTheory.v
@@ -6,7 +6,7 @@
 Require Import Reals.
 Require Import Coquelicot.Coquelicot.
 Require Import Psatz.
-Require Import MyUOR_H1.
+Require Import UOR_H1_HPO.
 Open Scope R_scope.
 
 (* We assume the spectral data {E n} and {alpha n} satisfy the required conditions.

diff --git a/coq/MellinTransform.v b/coq/MellinTransform.v
@@ -6,7 +6,7 @@
 Require Import Reals.
 Require Import Coquelicot.Coquelicot.
 Require Import Psatz.
-Require Import MyUOR_H1.
+Require Import UOR_H1_HPO.
 Open Scope R_scope.
 
 (* We define the spectral zeta function for H1 as:

diff --git a/coq/SelfAdjointness.v b/coq/SelfAdjointness.v
@@ -6,7 +6,7 @@
 Require Import Reals.
 Require Import Coquelicot.Coquelicot.
 Require Import Psatz.
-Require Import MyUOR_H1.  (* Contains definitions: H1, D_H1, in_D_H1, inner_product, etc. *)
+Require Import UOR_H1_HPO.  (* Contains definitions: H1, D_H1, in_D_H1, inner_product, etc. *)
 Require Import integration.
 Open Scope R_scope.
 

diff --git a/coq/ThetaInversion.v b/coq/ThetaInversion.v
@@ -6,7 +6,7 @@
 Require Import Reals.
 Require Import Coquelicot.Coquelicot.
 Require Import Psatz.
-Require Import MyUOR_H1.
+Require Import UOR_H1_HPO.
 Open Scope R_scope.
 
 (* Recall that the spectral trace is defined as: