diff options
| author | Enrico Tassi | 2018-10-29 11:17:13 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-29 11:17:13 +0100 |
| commit | 8d6e79649a3f7696977954de881671c23457c0f2 (patch) | |
| tree | 6d7d18de50dce4dea8a052143d5e954c6efe6e07 /library | |
| parent | 665146168720c094ce4fbb3d7d044d9904099f95 (diff) | |
| parent | e37a58ad110c13e3f6a8f4c27458e46a8ab36752 (diff) | |
Merge PR #8812: [ssreflect] Better use of Coqlib
Diffstat (limited to 'library')
| -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... *) |