coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] is there a metacoq email list?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] is there a metacoq email list?
Date: Fri, 8 Jan 2021 18:11:15 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f180.google.com
Ironport-phdr: 9a23:w1aQWhFfbT8Wd1YJi5/htp1GYnF86YWxBRYc798ds5kLTJ7yp8SwAkXT6L1XgUPTWs2DsrQY0rWQ6fy9EjNfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsswncuckbjYRgJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhyhqRJh3oDaY4abO/Vica3SZt4aWWhMU9xNWyFbHo+wcY0CBPcBM+ZCqIn9okMDoRW8BQmrAuPvyzxIiWHy3aIkzessCg7G3Ak6ENIPtHTYtsn6NKAXUey70aLFyjfDb/RQ2Tf864jHbBQhru+SUr9rfsrRzFMgFwLBjlmKtYPlODaV2/0LvmOG4OVuSfihhHQ7qwFtvDev3MEsh5HUio8Vyl7J+jt0zJopKNC4SkN2b8KpHZRMuyyaKod4TN8uTmVptSg6ybALp4K3cTQXxZg5xRPSd+GKfoaI7xztUuuaPDR2hGp9db6hmxq/9VKsx+78W8WuzVpHrytInsPRun0OyxDf8taLR/ph8ku83DuDygTe5f1BLE07lKfXN4Itz7stmpYNsUnOGyD7l1nqg6KWc0gr5Oal6+rpYrjjqJ+TKZJ7hR37P6szhMO/D+Y1Pw4TVGaB4+u8zqfs/UjhTbVKkPI2lq7ZvYjfJcsBp665BxZZ0ocn6xqiFjum3skUkHobIF5fdxKHiI/pO17KIP/mF/uwn1OskDJzy/DHOL3uHInNI2DdnLv9ebtx8U1RxQopwdxC5p9ZC6sNLO/wV0PtrNDYCwU2Mw2ww+bpEtV90YYeVHqNAq+eNqPSsFyI6fwrI+aSeoAYozn9K/0/6P7viX81g0MSfa6s3ZcPcnC3AuxmI1mFYXrrmtoODWAKvhMnQOP2jF2CTCVcam2pX6M84zE7EJipAZ3CRoCrmryB3T20EodYZmBcWRiwFiLjcJzBUPMRYmrGKch41zcASLKJSok71BjouhWsmJR9Ke+BsC8fs5Pg2dx46sXckBgz8Xp/CMHXmzWPSGd1nW4MSjIe06V2oEg7wVCGh/sry8dEHMBesqsaGjwxMoTRmrQjV4LCHznZd9LMc26IB828CGhoHN00yt4KJU16Hof610GR72+RG7YQ0oezKtkx+6PY0WL2Ip8kmXnD3aglyVIhR5kWbDD0tutE7wHWQrXxvQCZmqKtL/pO2SfM8CKCyTPLshgICEh/VqLKWX1ZbUzT/4z0

I'm getting some errors trying to install metacoq from opam. Is there
a metacoq email list I can request help from?

# Error: The implementation gen-src/cRelationClasses.ml
# [...]
# val eq_equivalence : ('a1, __) coq_Equivalence
# File "gen-src/cRelationClasses.mli", line 107, characters 0-46:
# Expected declaration
# File "gen-src/cRelationClasses.ml", line 204, characters 4-18:
# Actual declaration
# make[3]: *** [Makefile.plugin:664: gen-src/cRelationClasses.cmx]
Error 2 # make[2]: *** [Makefile.plugin:339: all] Error 2

[Coq-Club] is there a metacoq email list?, jonikelee AT gmail.com, 01/09/2021
- Re: [Coq-Club] is there a metacoq email list?, Yannick Forster, 01/09/2021