The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

Hi Tiwari,

Thank you very much for your reply! This is very helpful.

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Mon, Dec 24, 2018 at 10:43 AM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

Hi Cao,

Coq maintainers could give the answer more precisely, but based on my understanding standard library [1] lists theories [2], while the library (setoid_ring) you are looking for is in plugins directory [3].  If I am looking for documentation that is in plugin directory then I do a Google search (name of directory/file in plugin directory + coq ), but you can construct the url by yourself using the directory name (setoid_ring) with the coq file (Ring.v) (https://coq.inria.fr/library/Coq.setoid_ring.Ring.html).  Hope it helps.

Best,

Mukesh Tiwari

[1] https://coq.inria.fr/library/index.html

[2] https://github.com/coq/coq/tree/master/theories

[3] https://github.com/coq/coq/tree/master/plugins

On Mon, Dec 24, 2018 at 10:23 AM Cao Qinxiang <caoqinxiang AT gmail.com> wrote:

Hi all,

I am wondering whether there are some standard library folders missing on the page "https://coq.inria.fr/library/index.html". For example, I cannot find setoid_ring  on it. I am wondering where I can find a more complete list of standard libraries. Thank you very much!

Best,

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240