A better Program documentation. Include it in the generated stdlib doc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 4 insertions, 4 deletions

diff --git a/theories/Program/Heq.v b/theories/Program/Equality.v
index cd405219f..cd405219f 100644
--- a/theories/Program/Heq.v
+++ b/theories/Program/Equality.v
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index c6e5a64fb..40356a9c4 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 4dc50694f..39c5b7734 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 58ac9d90e..55784671f 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.