Update presup a bit

Beluga-lang · Sep 30, 2024 · d2a9e15 · d2a9e15
1 parent 96e7298
commit d2a9e15
Show file tree

Hide file tree

Showing 6 changed files with 289 additions and 246 deletions.
diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v
@@ -1,5 +1,5 @@
 From Coq Require Import Setoid.
-From Mcltt Require Import Base LibTactics CtxSub.
+From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Export SystemOpt.
 Import Syntax_Notations.
 

diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v
@@ -1,6 +1,6 @@
 From Coq Require Import Setoid Nat.
-From Mcltt Require Import Base LibTactics CtxSub.
-From Mcltt.Core Require Export SystemOpt CoreInversions.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Export CoreInversions.
 Import Syntax_Notations.
 
 Corollary sub_id_typ : forall Γ M A,

diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v
@@ -1,5 +1,5 @@
-From Mcltt Require Import Base LibTactics CtxSub.
-From Mcltt Require Export System.
+From Mcltt Require Import Base LibTactics.
+From Mcltt Require Export CtxSub.
 Import Syntax_Notations.
 
 Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.