diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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" |