Skip to content

Commit

Permalink
Remove code that has been deprecated for a while.
Browse files Browse the repository at this point in the history
  • Loading branch information
ppedrot authored and damien-pous committed Oct 22, 2024
1 parent 131b98a commit f429176
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,14 @@ let fresh_name env n =
annotR 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 "RelationAlgebra.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 f429176

Please sign in to comment.