The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I somewhat recently discovered CoqMT (http://pierre-yves.strub.nu/coqmt/), and am interested in playing around with it.  In particular, I'm curious, can it be extended to prototype ideas for adding in judgmental commutation rules for [match] constructs, or other decidable rules?  Is there a user-guide somewhere for how to use it and/or extend it?  Also, is there a version that works with Coq 8.4?

Thanks,

Jason