Fix dependency bugs due to Program modules renamings.

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

4 files changed, 7 insertions, 7 deletions

diff --git a/Makefile.common b/Makefile.common
index 1325eabcf1..ac4233e4a4 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -751,8 +751,8 @@ CCVO:=
 
 DPVO:=contrib/dp/Dp.vo
 
-SUBTACVO:=theories/Program/Tactics.vo theories/Program/Heq.vo \
-	theories/Program/Utils.vo theories/Program/FixSub.vo theories/Program/Program.vo \
+SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo \
+	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \
 	theories/Program/FunctionalExtensionality.vo
 
 RTAUTOVO:= \
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index d38bdb79ef..1d10405c9d 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -95,7 +95,7 @@ let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
 (*   check_required_library ["Coq";"Logic";"JMeq"]; *)
-  require_library "Coq.Program.FixSub";
+  require_library "Coq.Program.Wf";
   require_library "Coq.Program.Tactics";
   require_library "Coq.Logic.JMeq";
   let env = Global.env () in
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index e5ac65878d..2335d3a253 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -13,7 +13,7 @@ let ($) f x = f x
 let contrib_name = "Program"
 
 let subtac_dir = [contrib_name]
-let fix_sub_module = "FixSub"
+let fix_sub_module = "Wf"
 let utils_module = "Utils"
 let fixsub_module = subtac_dir @ [fix_sub_module]
 let utils_module = subtac_dir @ [utils_module]
@@ -28,8 +28,8 @@ let make_ref l s = lazy (init_reference l s)
 let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
-let fix_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_sub"
-let fix_measure_sub_ref = make_ref [contrib_name;"FixSub"] "Fix_measure_sub"
+let fix_sub_ref = make_ref fixsub_module "Fix_sub"
+let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
 let lt_ref = make_ref ["Init";"Peano"] "lt"
 let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
 let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 1915ad37cb..f0c67df3a2 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -13,5 +13,5 @@ Require Export Logic.
 Require Export Datatypes.
 Require Export Specif.
 Require Export Peano.
-Require Export Wf.
+Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.