#605024 coq: coq.el requires nonexistent hilit19

Package:
coq
Source:
coq
Description:
proof assistant for higher-order logic (toplevel and compiler)
Submitter:
Hendrik Tews
Date:
2022-06-14 05:57:04 UTC
Severity:
normal
#605024#5
Date:
2010-11-26 13:40:14 UTC
From:
To:
The file /etc/emacs/site-start.d/50coq.el sets coq-mode for *.v
files and declares coq-mode to autoload coq.el. The file
/usr/share/emacs/site-lisp/coq/coq.el however requires hilit19 in
line 140, which seems not to be available in squeeze. Therefore
loading any *.v file or starting coq-mode manually stops with the
error

  File mode specification error: (file-error "Cannot open load file" "hilit19")

This problem is wrongly attributed to proofgeneral, see #605014
and #582768.


Bye,

Hendrik
#605024#10
Date:
2010-11-26 14:17:52 UTC
From:
To:
reassign 605014 coq
reassign 582768 coq
forcemerge 605024 605014 582768
thanks

This seems to be fixed in Coq 8.3 (in experimental). We will try to
backport a fix and ask the Release Team for an unblock.

Right. I'm merging the bugreports.

Regards,
#605024#17
Date:
2010-11-27 09:35:46 UTC
From:
To:
Le 26/11/2010 15:17, Mehdi Dogguy a écrit :

Unfortunately, the emacs mode in v8.3 has completely changed, and I
cannot guarantee that it works with v8.2:


Cheers,
#605024#18
Date:
2022-06-14 05:55:27 UTC
From:
To:
Hi,

the recent coq versions don't ship any coq for emacs file, so this bug
is now obsolete.

Cheers,

J.Puydt