Update minor

Beluga-lang · Jun 4, 2024 · ce40dc1 · ce40dc1
1 parent f622f71
commit ce40dc1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Presup Syntactic.Corollaries Evaluation Readback PER.
+From Mcltt.Core Require Import Evaluation PER Presup Readback Syntactic.Corollaries.
 
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.