Folding eats comments before next definition

[wilcoxjay]

Consider the following code

(* a foo is a nat *) 
Definition foo := nat.

(* bar increments a foo *)
Definition bar (x : foo) : foo := S x.

If I then fold the definition of foo, the documenting comment on bar also gets hidden. Is it possible to prevent this, or have an option that prevents this?

[cpitclaudel]

It would be nice :) That folding is handled by outline-minor-mode. Do you want to have a look at whether it supports the kind of feature that you described? (I think it doesn't, but we could double-check)

I've been wanting to experiment with origami.el, but I haven't really had time to do so; see gregsexton/origami.el#20. The scary part is the parse tree; it's more or less impossible to get a parse tree of a Coq document at the moment.