diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 827747c6b8..f504b0734f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -473,13 +473,13 @@ exception ToShow of exn let jmeq () = try - Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; + Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq" with e when Errors.noncritical e -> raise (ToShow e) let jmeq_refl () = try - Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; + Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl" with e when Errors.noncritical e -> raise (ToShow e) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d2d5a957f4..857e82fc59 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -150,7 +150,7 @@ let coq_S = function () -> (coq_base_constant "S") let lt_n_O = function () -> (coq_base_constant "lt_n_O") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> (constr_of_global (delayed_force max_ref)) -let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" +let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; |