Rearrange soundness proofs (#155)

Beluga-lang · Aug 17, 2024 · 1fb5188 · 1fb5188
1 parent 6050e64
commit 1fb5188
Show file tree

Hide file tree

Showing 12 changed files with 1,410 additions and 1,273 deletions.
diff --git a/theories/Core/Soundness/Cumulativity.v b/theories/Core/Soundness/Cumulativity.v
diff --git a/theories/Core/Soundness/EquivalenceLemmas.v b/theories/Core/Soundness/EquivalenceLemmas.v
diff --git a/theories/Core/Soundness/LogicalRelation.v b/theories/Core/Soundness/LogicalRelation.v
@@ -1 +1 @@
-From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas.
+From Mcltt.Core.Soundness Require Export LogicalRelation.Core LogicalRelation.Lemmas.
diff --git a/theories/Core/Soundness/LogicalRelation/Core.v b/theories/Core/Soundness/LogicalRelation/Core.v
@@ -0,0 +1 @@
+From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.CoreLemmas.
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas.
		From Mcltt.Core.Soundness Require Export LogicalRelation.Core LogicalRelation.Lemmas.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.CoreLemmas.