Opened 8 years ago
Closed 8 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 8 years ago by
comment:2 Changed 8 years ago by
| Resolution: | → invalid |
|---|---|
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Sorry, this is in fact a problem of company-coq.