Opened 4 years ago

Closed 4 years ago

#511 closed defect (invalid)

new Coq command "From" supported by PG?

Reported by: coquser Owned by: David Aspinall
Priority: blocker Milestone: PG-Emacs-4.4
Component: 2:pg-emacs Keywords:
Cc: frederic.blanqui@…

Description

When trying to use the new Coq command "From" (https://coq.inria.fr/distrib/V8.5pl1/refman/Reference-Manual008.html#hevea_command116), I get:

Error: Unknown command of the non proof-editing mode.

Change History (2)

comment:1 Changed 4 years ago by coquser

Sorry, this is in fact a problem of company-coq.

comment:2 Changed 4 years ago by coquser

Resolution: invalid
Status: newclosed
Note: See TracTickets for help on using tickets.