From 59d41299f2b8c2a9968ac8192d052642daf00e76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Mon, 21 Oct 2024 18:22:04 +0200 Subject: [PATCH] Remove code that has been deprecated for a while. --- src/reify.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/reify.ml b/src/reify.ml index 2e6231f..0ebd202 100644 --- a/src/reify.ml +++ b/src/reify.ml @@ -27,8 +27,14 @@ let fresh_name n env = vname, mkVar vname (* access to Coq constants *) +let find_reference path id = + (* TODO: use registering rather than constant hardwiring *) + let path = DirPath.make (List.rev_map Id.of_string path) in + let fp = Libnames.make_path path (Id.of_string id) in + Nametab.global_of_path fp + let get_const dir s = - lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (Coqlib.find_reference "ATBR.reification" dir s))) + lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (find_reference dir s))) (* make an application using a lazy value *) let force_app f = fun x -> mkApp (Lazy.force f,x)