Skip to content

Commit

Permalink
Merge pull request #45 from ppedrot/rm-deprecated-coqlib
Browse files Browse the repository at this point in the history
Remove code that has been deprecated for a while.
  • Loading branch information
ppedrot authored Oct 21, 2024
2 parents 5e3f4fe + 59d4129 commit 47ac8fb
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/reify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 47ac8fb

Please sign in to comment.