CI is stubborn

Beluga-lang · May 21, 2024 · 624dcbb · 624dcbb
1 parent 9f881e3
commit 624dcbb
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
@@ -1,5 +1,5 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
-From Mcltt Require Import Base LibTactics LogicalRelation System.
+From Mcltt Require Import Base LibTactics Completeness.LogicalRelation System.
 Import Domain_Notations.
 
 Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},

diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v
@@ -1,5 +1,5 @@
 From Coq Require Import Morphisms_Relations.
-From Mcltt Require Import Base LibTactics LogicalRelation.
+From Mcltt Require Import Base LibTactics Completeness.LogicalRelation.
 Import Domain_Notations.
 
 Lemma valid_typ : forall {i Γ},

diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
@@ -1,5 +1,5 @@
 From Coq Require Import Morphisms_Relations Relations.
-From Mcltt Require Import Base LibTactics LogicalRelation System.
+From Mcltt Require Import Base LibTactics Completeness.LogicalRelation System.
 Import Domain_Notations.
 
 Lemma valid_lookup : forall {Γ x A env_rel}