coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Duplicated definition in standard library

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Duplicated definition in standard library
Date: Mon, 25 Mar 2019 14:32:12 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f48.google.com
Ironport-phdr: 9a23:NDajlxZdrKMJNKv/cWFDlbH/LSx+4OfEezUN459isYplN5qZoMy5bnLW6fgltlLVR4KTs6sC17OO9f+/EjFQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5uIBmsrwjctMYajIthJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1UrhKvqRJ83oDafp2aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb5EPD+0EPetAsYTyvVwOpgalCwmtAuPuxT5IiWXw3a01zu8sFh3J0xYnH9IXsXTUqtr0NKYIXuCzw6nF1jrDb/ZM1jf87IjEaAwuofaJXb9pd8fa1EohFxvdg1mOtYDoOymZ2+cNvmSB8eZsSP6jh3QopgxypDWk290ihZPTho0Pz1DJ7SV5z5gxJd2/UEN7ZMSrEJpUty2DMIt2Xt4uT3hmuCs1ybAKo5G7fC8NyJQowx7QdeaLfJSP4hLmTOqRIDF4i2x5eL+nmRq+7Uytxvf/W8S0ylpGsDdJnsXWun0C1BHf8s2HReF8/kel1zaPzQfT6uRcLE8oj6XbLIchwr82lpscsETMBCn2mErtga+Zc0Ur4Omo6+D9brr6oZ+cMpd4ihviPaQ2hsy/HeM4PxASUGic4OSwzaHs/UnkQLpRlfA2ianYsJXCJcsBvKK5AglV0pwi6xmlFTum3s4YzjE7KwdOfwvChIz0MXnPJur5BLGxmQeCijBuktvPOfXYA5PdL3HFn/+1dr968k9a2As6y9936JddC7VHK/X2DByi/OfEBwM0ZlTni93sD89wg9tHCDC/R5SBOaaXimemo+cmIu2CfogQ4W+vJP0s5vqohng8ywZEIfuZmKAPYXX9JcxIZl2DaCO10NgEGGYO+AE5Sb6y0QDQYXtof3+3GpkEyHQ7BYahV9qRQ4mshPmGwH7+EMEGIG9BDV+IHDHjcIDWA/o=

Dear Coq clubbers,

I find it really annoying that similar definitions appear more than once in Coq's standard library. For example, reflexive and transitive appear both in Classes.RelationClasses and Relations.Relation_Definitions.

In this case, is there any suggestion which one should I use? Also, is there a plan in Coq development team to merge such definitions?

Best,

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

[Coq-Club] Duplicated definition in standard library, Cao Qinxiang, 03/25/2019
- Re: [Coq-Club] Duplicated definition in standard library, Théo Zimmermann, 03/25/2019
  - Re: [Coq-Club] Duplicated definition in standard library, Cao Qinxiang, 03/26/2019
  - Re: [Coq-Club] Duplicated definition in standard library, Pierre Casteran, 03/26/2019