coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Company-coq possible issue?

From: Chris Brinkley <Chris.Brinkley AT sslmda.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Company-coq possible issue?
Date: Tue, 31 Oct 2017 01:33:51 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Chris.Brinkley AT sslmda.com; spf=None smtp.mailfrom=Chris.Brinkley AT sslmda.com; spf=None smtp.helo=postmaster AT mx0a-00142601.pphosted.com
Ironport-phdr: 9a23:OYwgERS9SIsSC7R5BMr43rxuDtpsv+yvbD5Q0YIujvd0So/mwa67bBGN2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnZBUin4YEB+If2wEYrPhey20fqz8tvdeU8A0DG6ePZ5KAi8hQTXrMgfx4V4fPUf0BzM91BIYeVNjUlyJFSQmxvtrpOb/IRi6GJ6ofMn9MpNQI3hZKA9QbUeBzMjZTNmrPb3vAXOGFPcrkAXVX8bx0JF

Now that I have ProofGeneral working with opam update of coq, I noticed on executing the trivial

Definition plus_fact : P := 2 + 2 = 4.

I get a company-coq error that disappears when I execute the next line:

company-coq: Parsing of tactic grammar failed with error (error Tactic parsing failure [(tactic: auto_using (quote AND) ))]”).

This is with ProofGeneral 4.4.1~pre, coq 8.6.0 installed per official coq opam intructions, and Logic.v from SF 5.3.

I don’t yet know if anything else is impacted. Should I be concerned?

This message (including any attachments) may contain confidential information intended for a specific individual and purpose. If you are not the intended recipient, you should delete this message and any attachments.

[Coq-Club] Company-coq possible issue?, Chris Brinkley, 10/31/2017
- Re: [Coq-Club] Company-coq possible issue?, Merlin Göttlinger, 10/31/2017