The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

Thank you very much!

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Mon, Mar 25, 2019 at 6:23 PM Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

Hi,

I'd recommend you use the version in Classes.RelationClasses. Defining
instances of the classes defined there should allow you to
subsequently use the reflexivity and transitivity tactics.

I was actually unaware of the existence of
Relations.Relation_Definitions. After looking at the log of this file,
I can tell you that it has been largely untouched since its creation
in the archive in 2000 (and then maybe it was already a copy-paste
from an older file). I don't know if there are any parts of this file
that are still useful to people and not duplicated elsewhere, but I
think it would be good to open an issue on the GitHub repository to
suggest its deprecation.

Best,
Théo

Le lun. 25 mars 2019 à 07:33, Cao Qinxiang <caoqinxiang AT gmail.com> a écrit :
>
> 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
>