diff options
Diffstat (limited to 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 3df071aff..6c4d76340 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -99,10 +99,6 @@ let init_constant dir s = let d = "Init"::dir in check_required_library (coq::d); gen_constant "Coqlib" d s -let logic_constant dir s = - let d = "Logic"::dir in - check_required_library (coq::d); gen_constant "Coqlib" d s - let logic_reference dir s = let d = "Logic"::dir in check_required_library ("Coq"::d); gen_reference "Coqlib" d s @@ -139,9 +135,6 @@ let logic_type_module = make_dir logic_type_module_name let datatypes_module_name = init_dir@["Datatypes"] let datatypes_module = make_dir datatypes_module_name -let arith_module_name = arith_dir@["Arith"] -let arith_module = make_dir arith_module_name - let jmeq_module_name = [coq;"Logic";"JMeq"] let jmeq_module = make_dir jmeq_module_name @@ -273,9 +266,6 @@ let build_coq_eq_data () = trans = Lazy.force coq_eq_trans; congr = Lazy.force coq_eq_congr } -let make_dirpath dir = - Names.make_dirpath (List.map id_of_string dir) - let build_coq_eq () = Lazy.force coq_eq_eq let build_coq_eq_refl () = Lazy.force coq_eq_refl let build_coq_eq_sym () = Lazy.force coq_eq_sym |