diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v (renamed from theories/Program/Heq.v) | 0 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 2 | ||||
| -rw-r--r-- | theories/Program/Program.v | 4 | ||||
| -rw-r--r-- | theories/Program/Wf.v (renamed from theories/Program/FixSub.v) | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/theories/Program/Heq.v b/theories/Program/Equality.v index cd405219f6..cd405219f6 100644 --- a/theories/Program/Heq.v +++ b/theories/Program/Equality.v diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index c6e5a64fb3..40356a9c49 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -1,5 +1,5 @@ Require Import Coq.Program.Utils. -Require Import Coq.Program.FixSub. +Require Import Coq.Program.Wf. (** The converse of functional equality. *) diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 4dc50694fa..39c5b77341 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,3 +1,3 @@ Require Export Coq.Program.Utils. -Require Export Coq.Program.FixSub. -Require Export Coq.Program.Heq.
\ No newline at end of file +Require Export Coq.Program.Wf. +Require Export Coq.Program.Equality. diff --git a/theories/Program/FixSub.v b/theories/Program/Wf.v index 58ac9d90ee..55784671f5 100644 --- a/theories/Program/FixSub.v +++ b/theories/Program/Wf.v @@ -1,4 +1,4 @@ -Require Import Wf. +Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. |