coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] extract logical path name of a .vo file

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] extract logical path name of a .vo file
Date: Tue, 23 Nov 2021 10:26:50 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f44.google.com
Ironport-data: A9a23:0yDvPKqGaP04rjpWZPnEQZN+lpFeBmJ4ZBIvgKrLsJaIsI5as4F+vmIXW23XM62CamekKosjPIy/pElUu5OBz9ZjS1BprXwzZn8b8sCt6faxfh6hZXvKRiHgZBs6tJtGMoGowPjZ/xYwnz/1WlTahSQ6hf7gqobUUraeY3koH1Q8E0/NtDo68wIHqt4w6TSGK1jV0T/Ci5W31G6Ng1aYAEpMg06wgE8HUMDJhd8tlgdWicanE7PpvyJ94Jo3fcldJpZjK2VeNrbSq+3rlNlV8o5FlirBBO9Jkp6jGqELarvbPAzLi30PHqb+3l5NoSs91qt9P/0ZAatVo2/RzpYhlZMU68L2FVtB0q7kwIzxVzFaEiQ4M6BG4rvKCXe6uM2XiUbBdhMAxt0zUBBqZ9NDkgpwKTgWqaZwxCo2RhuEnqe9xK+xYvJ9g9wqasjtJoIW/H96pQw1p94yGcWZBfrevIoAmm8k3JUWW6yPNpMNMm83KknUPEhmJHM8DbYSnMOJj1/DaRlmqXeB/PJiuCyKlBgZPKPFNdPUfpmLQpwQkBrE4G3B+Gv9D1cRM9n39NZMyVr07senoM8xcNh6+HyEGv9WbJm7w2USDFgXUgL+r6XlzEG5XN1bJgof/S9GQW0anKC0ZoGVYvF6iCfsUt0gtx54HOgz6QXLwa3Ri+pcLnZRVSZPMbTKq+dvLQHHFTa1cxfBCjlmsbnTQnWYnltRhVteJgBNRVI/ieQ4ocfpLjUtTEzfTv4Cczq7LJOIsw==
Ironport-hdrordr: A9a23:nIplTqtvURkg7ucTJcz94Ok77skDZ9V00zEX/kB9WHVpm6uj9vxG/c516faQsl0ssR4b+exoVJPwI080lqQa3WBuB9qftWDd0QPDEGgI1/qG/9SPIVycyge+78tdT5Q=
Ironport-phdr: A9a23:occ28h/90GjWI/9uWc+8ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZQqDu7401QeBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdm72/q99pDSbAlEmSexba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWVOXshTWCJBDI2ybJYBAfQdMutDtYbxu0EDoAGiCQWwBu7izCJDiH/s3a091uQsCQXI3A0lH9kTsHrbstX1NL0WUe+r0aLFyjfDb/JT2Tvn5ojHbBAhoeuIXb1uasfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFvWv6hhXQ9pAFtvjig2N0sio/Ri48JyV3J6yF0zYk0KNC8SkN3fcCpHpVUui2GK4Z7Rt8uTmBmtSs71LALp4K3cSwOxZklyBPRZeGKfYeV7x/9SOqcJypzinF9eL+nmRq+7Uytxvf/W8S0ylpGsytIn9jWun0C2BHe7NWMROFn8Ue7wzmP0hje6uFaLkAwkqrWM5shzaQxlpoXqEjDHyj2lFjvgK+YeUgp9fKk6+vgYrXhqZ+cM5F7hhviPaQpn8yzGeU4Mg4QUGiH4emwyqHv8EnjTLhJjvA6iLTVvZHbKMgBqaO0DBdZ0oM55Ba+Czem3s4YnX4CLF9dehKHjo3pN0vAIP/mDfe/mVCsnylwyvDJO73uGJTNLnzZnLj9erZ97lZQyBAvwtBH+5JUFrYBLervVU/2rdzUFwM2Mwipw+n8E9h9zYMfWWeXAqCDKq/SsFmI5vguI+aWfoMVtiz9eLAZ4KvFimZxslsAd+H91pwOLXu8A/5OIkODYHOqjM1XQkkQuQ9rbu3vwHOPUSRXaj7mXaM5oD82CJiiAK/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZLXvKeqeJdxQLULGgT8kq0hT87GcSKpJiJ+vQvywf7NftiIQz6OrUmhU/szdzCpbFu4liZ25xl2IMATQx2fImyXE=

A Coq command or a seperate executable? How about Locate?

Locate Arith. (* Module Coq.Arith.Arith *)

[Coq-Club] extract logical path name of a .vo file, Abhishek Anand, 11/23/2021
- Re: [Coq-Club] extract logical path name of a .vo file, Jim Fehrle, 11/23/2021
  - Re: [Coq-Club] extract logical path name of a .vo file, Jason Gross, 11/23/2021