diff options
| author | Vincent Laporte | 2018-10-16 11:21:38 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 09:51:53 +0000 |
| commit | e37a58ad110c13e3f6a8f4c27458e46a8ab36752 (patch) | |
| tree | 7d84c3386bc093bf32d996b24243a3bf1df4d523 /library/coqlib.ml | |
| parent | 5b690354c203f33be3eb33a6d905a64ab6ae4430 (diff) | |
[Coqlib] Remove redundant check
Diffstat (limited to 'library/coqlib.ml')
| -rw-r--r-- | library/coqlib.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index a044a9a395..784360dc8a 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -227,8 +227,7 @@ type coq_eq_data = { (* Leibniz equality on Type *) -let build_eqdata_gen lib str = - let _ = check_required_library lib in { +let build_eqdata_gen str = { eq = lib_ref ("core." ^ str ^ ".type"); ind = lib_ref ("core." ^ str ^ ".ind"); refl = lib_ref ("core." ^ str ^ ".refl"); @@ -237,9 +236,9 @@ let build_eqdata_gen lib str = congr = lib_ref ("core." ^ str ^ ".congr"); } -let build_coq_eq_data () = build_eqdata_gen logic_module_name "eq" -let build_coq_jmeq_data () = build_eqdata_gen jmeq_module_name "JMeq" -let build_coq_identity_data () = build_eqdata_gen datatypes_module_name "identity" +let build_coq_eq_data () = build_eqdata_gen "eq" +let build_coq_jmeq_data () = build_eqdata_gen "JMeq" +let build_coq_identity_data () = build_eqdata_gen "identity" (* Inversion data... *) |