dependency clean-ups

CoqHott · Feb 11, 2025 · cf22d43 · cf22d43
1 parent 43f28a3
commit cf22d43
Show file tree

Hide file tree

Showing 12 changed files with 17 additions and 14 deletions.
diff --git a/theories/Fundamental.v b/theories/Fundamental.v
@@ -1,6 +1,6 @@
 (** * LogRel.Fundamental: declarative typing implies the logical relation for any generic instance. *)
 From LogRel Require Import Utils Syntax.All GenericTyping DeclarativeTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Escape Irrelevance Reflexivity Transitivity Universe Weakening Neutral Induction NormalRed.
+From LogRel.LogicalRelation Require Import Escape Irrelevance Reflexivity Transitivity Weakening Neutral Induction NormalRed.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion Reflexivity SingleSubst Escape.
 From LogRel.Validity.Introductions Require Import Application Universe Pi Lambda Var Nat Empty SimpleArr Sigma Id.
 

diff --git a/theories/LogicalRelation/Introductions/Id.v b/theories/LogicalRelation/Introductions/Id.v
@@ -1,5 +1,5 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Escape Irrelevance Weakening Neutral Reflexivity NormalRed Reduction Transitivity Universe EqRedRight.
+From LogRel.LogicalRelation Require Import Induction Escape Irrelevance Weakening Neutral Reflexivity NormalRed Reduction Transitivity EqRedRight Introductions.Universe.
 
 Set Universe Polymorphism.
 Set Printing Primitive Projection Parameters.

diff --git a/theories/LogicalRelation/Introductions/SimpleArr.v b/theories/LogicalRelation/Introductions/SimpleArr.v
@@ -1,6 +1,6 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity Application.
-From LogRel.LogicalRelation.Introductions Require Import Poly Pi.
+From LogRel.LogicalRelation Require Import Induction Irrelevance Weakening Neutral Escape Reflexivity NormalRed Reduction Transitivity.
+From LogRel.LogicalRelation.Introductions Require Import Poly Pi Application.
 
 Set Universe Polymorphism.
 Set Printing Primitive Projection Parameters.

diff --git a/theories/Validity/Introductions/Application.v b/theories/Validity/Introductions/Application.v
@@ -1,5 +1,5 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction Application.
+From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction Introductions.Application.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity.
 
 Set Universe Polymorphism.

diff --git a/theories/Validity/Introductions/Empty.v b/theories/Validity/Introductions/Empty.v
@@ -1,6 +1,7 @@
 From Coq Require Import CRelationClasses.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import  Induction  Escape Irrelevance Reflexivity Irrelevance Weakening Neutral Transitivity Reduction Application Universe EqRedRight SimpleArr.
+From LogRel.LogicalRelation Require Import  Induction  Escape Irrelevance Reflexivity Irrelevance Weakening Neutral Transitivity Reduction EqRedRight.
+From LogRel.LogicalRelation.Introductions Require Import Application Universe.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity Reduction Universe Pi SimpleArr Var Application.
 
 Set Universe Polymorphism.

diff --git a/theories/Validity/Introductions/Id.v b/theories/Validity/Introductions/Id.v
@@ -1,5 +1,6 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Irrelevance Weakening Neutral Transitivity Reduction Application Universe Id EqRedRight NormalRed InstKripke.
+From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Irrelevance Weakening Neutral Transitivity Reduction EqRedRight NormalRed InstKripke.
+From LogRel.LogicalRelation.Introductions Require Import Universe Id.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity Reduction Universe Var Poly.
 
 Set Universe Polymorphism.

diff --git a/theories/Validity/Introductions/Lambda.v b/theories/Validity/Introductions/Lambda.v
@@ -1,5 +1,5 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Neutral Weakening Irrelevance Application Reduction Transitivity NormalRed EqRedRight InstKripke.
+From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Neutral Weakening Irrelevance Introductions.Application Reduction Transitivity NormalRed EqRedRight InstKripke.
 From LogRel.Validity Require Import Validity Irrelevance Properties SingleSubst Reflexivity Conversion Reduction Pi Application Var.
 
 Set Universe Polymorphism.

diff --git a/theories/Validity/Introductions/Nat.v b/theories/Validity/Introductions/Nat.v
@@ -1,5 +1,6 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction  Escape Irrelevance Reflexivity Irrelevance Weakening Neutral Transitivity Reduction Application Universe EqRedRight SimpleArr.
+From LogRel.LogicalRelation Require Import Induction  Escape Irrelevance Reflexivity Irrelevance Weakening Neutral Transitivity Reduction EqRedRight.
+From LogRel.LogicalRelation.Introductions Require Import Universe SimpleArr Application.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity Reduction Universe Pi SimpleArr Var Application.
 
 Set Universe Polymorphism.

diff --git a/theories/Validity/Introductions/Sigma.v b/theories/Validity/Introductions/Sigma.v
@@ -1,7 +1,7 @@
 From Coq Require Import ssrbool CRelationClasses.
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Irrelevance Weakening Neutral Transitivity Reduction Application Universe EqRedRight SimpleArr NormalRed InstKripke.
-From LogRel.LogicalRelation.Introductions Require Import Poly.
+From LogRel.LogicalRelation Require Import Induction Escape Reflexivity Irrelevance Weakening Neutral Transitivity Reduction EqRedRight NormalRed InstKripke.
+From LogRel.LogicalRelation.Introductions Require Import Application Universe Poly.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion SingleSubst Reflexivity Reduction Universe Poly.
 
 

diff --git a/theories/Validity/Introductions/SimpleArr.v b/theories/Validity/Introductions/SimpleArr.v
@@ -1,6 +1,6 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
 From LogRel.LogicalRelation Require Import Escape Reflexivity Neutral Weakening Irrelevance.
-From LogRel.Validity Require Import Validity Irrelevance Properties Pi Application Lambda Var.
+From LogRel.Validity Require Import Validity Irrelevance Properties Pi Application Var.
 
 Set Universe Polymorphism.
 

diff --git a/theories/Validity/Introductions/Universe.v b/theories/Validity/Introductions/Universe.v
@@ -1,5 +1,5 @@
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Reduction Universe.
+From LogRel.LogicalRelation Require Import Induction Irrelevance Escape Reflexivity Weakening Neutral Transitivity Introductions.Universe.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion Reflexivity.
 
 Set Universe Polymorphism.

diff --git a/theories/Validity/Introductions/Var.v b/theories/Validity/Introductions/Var.v
@@ -1,6 +1,6 @@
 (** * LogRel.Introductions.Var : Validity of variables. *)
 From LogRel Require Import Utils Syntax.All GenericTyping LogicalRelation.
-From LogRel.LogicalRelation Require Import Escape Irrelevance Reflexivity Transitivity Universe Weakening Neutral Induction NormalRed.
+From LogRel.LogicalRelation Require Import Escape Irrelevance Reflexivity Transitivity Introductions.Universe Weakening Neutral Induction NormalRed.
 From LogRel.Validity Require Import Validity Irrelevance Properties Conversion Reflexivity SingleSubst Escape.
 
 Set Universe Polymorphism.