Tuareg-mode doesn't really work for mlg file

HuStmpHrrr · December 18, 2025, 7:46pm

However, in the same tutorial, when I open rocq/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg at master · rocq-prover/rocq · GitHub, my emacs highlights DECLARE, and make the whole file unreadable.

How did you set things up?

SkySkimmer · December 20, 2025, 1:47pm

IDK, it just works for me and I don’t think I did anything special for it .emacs.d/config.org at master · SkySkimmer/.emacs.d · GitHub

Topic		Replies	Views
Learning to write Coq plugins - what is the purpose of .mlg files? Developing plugins	5	190	June 7, 2024
How do I solve "no implementation available for ..."? Developing plugins	1	914	October 8, 2019
Best way to deal with mlg files warning-as-errors in plugins built by dune? Developing plugins	3	110	June 22, 2024
[PG/Company] Structured outline mode Using Rocq	2	513	April 23, 2020
How can an OCaml tactic return something else than unit? Developing plugins	1	725	April 29, 2020