diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f922b2f600..3dfce8bf48 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -460,7 +460,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match wf_rel_expr_opt with | None -> let ltof = - let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) in + let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) in Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 2d50adf00c..5942e11b49 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -132,7 +132,7 @@ let coq_constant s = Coqlib.init_modules s;; let find_reference sl s = - (Nametab.locate (make_qualid(Names.make_dirpath + (Nametab.locate (make_qualid(Names.Dir_path.make (List.map Id.of_string (List.rev sl))) (Id.of_string s)));; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 28752fe4fd..68c5e16ae1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -50,7 +50,7 @@ let coq_base_constant s = (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;; let find_reference sl s = - (locate (make_qualid(Names.make_dirpath + (locate (make_qualid(Names.Dir_path.make (List.map Id.of_string (List.rev sl))) (Id.of_string s)));; @@ -85,7 +85,7 @@ let type_of_const t = let constant sl s = constr_of_global - (locate (make_qualid(Names.make_dirpath + (locate (make_qualid(Names.Dir_path.make (List.map Id.of_string (List.rev sl))) (Id.of_string s)));; let const_of_ref = function |