coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?
Date: Wed, 29 Mar 2017 11:02:01 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-b.ensmp.fr
Ironport-phdr: 9a23:g8rgsByXS8kLlZfXCy+O+j09IxM/srCxBDY+r6Qd2+sRIJqq85mqBkHD//Il1AaPBtSHraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pncbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfWC5GAoOyYYQBAekPMulEoIfyvFYOsQK+CBOwCO/z0DJFhHn71rA63eQ7FgHG2RQtEMwVvXXbr9j5KL0eUeevzKnH0D7Pa/xY2TL86IjMcxAhpuyHU7ZufsrK01EvDB7OgFSKpozhOzOayOsNs2+G5Od8T+KvinQoqxp0rjWp28wihI7JhocPxVDF8yV02Jw1KsO5SE51e9KkFZ9QuieHPIV1WsMvW3xktSI1x7Ecp5K3YScHxI46yxPfaPGLaZWE7xziWeqJJTp0mmhpdbajixqo70Ss1vfwW8213VtMsyFLiMPDtmoX2BzW8sWHSuVy/kOm2TuXyw/c9vhIIVwplarDMZEhxKc8loAUsUvZGy/2mUP2jKCPeko/4OSn9eLnYq7jpp+ELYN0hBv+Prwvmsy5H+s4LhADU3Wf9OmzzrHv41D1TbpQgvErkqTUs4rWKdkVq6O4GwNV15ws6xe7DzeoytQYmnwHIUpbdx+cgInkOE3CLOr/DfeljFSgiC1ryOzePr39HpXNKWDOn6vmfbZk8kJT1A4zzc1E6J9PEbEAIPfzWlfru9DCDx85NRa0w+f9B9ln2IMeQzHHPqjMEqrJtlnAyfgoOPLEMI0cozH7JOIi/OW/pXA8kF4ZO6Ku2M1ERmq/G6FrC1XJOTzrmNhJUUoPvw4/S6TIhUYQSnZ8bnK2Uq07rhghCYu9TNSQDruxiaCMiX/oVqZdYXpLXxXVSS/l
Organization: X80 Heavy Industries

e AT x80.org
(Emilio Jesús Gallego Arias) writes:

> Did you do `open Ltac_plugin` in reif.ml, as instructed in
> `dev/doc/changes.txt` ?

s/reif.ml/reif.ml4/

I just had a look to your code, yup, that seems like the culprit, now
ltac is a plugin and you must open the packed module in every file using
ltac.

E.

[Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Jason Gross, 03/29/2017
- Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Emilio Jesús Gallego Arias, 03/29/2017
  - Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Emilio Jesús Gallego Arias, 03/29/2017
    - Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Jason Gross, 03/29/2017