diff --git a/theories/Fundamental.v b/theories/Fundamental.v index aff66e82..75cb6d6a 100644 --- 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 index 0a80c824..17c857df 100644 --- 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 index c784570b..f556fd0c 100644 --- 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 index 4f212b7a..09fb04f7 100644 --- 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 index 42afcec7..832876c8 100644 --- 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 index fc8e5d62..f8a35af5 100644 --- 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 index 3ef74142..892dc378 100644 --- 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 index 2feab573..ec3468fb 100644 --- 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 index 475da557..82b5617e 100644 --- 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 index 1e87fbca..57bbc7e0 100644 --- 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 index 9c0f9be2..a67d2614 100644 --- 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 index d9818d3d..019634f3 100644 --- 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.