diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-08 15:32:36 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-08 15:32:36 +0000 |
| commit | 81428d74f493b04b65889a309c24e4c9a1e5762f (patch) | |
| tree | 3ddfd59102e6cccf1ef39186a1efb3508acc116b /contrib | |
| parent | 2e3a264122b79d8c97adcddfc4e120c343493e28 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index d38bdb79e..1d10405c9 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 e5ac65878..2335d3a25 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" |