Enrico Tassi wrote: > I'm interested in that software, but I'm a bit worried on how the > package could be done. Last time I used it, it was necessary to generate > a new coq toplevel... Is it now possible to load it on the fly?
It will be with the combination Coq 8.2 / OCaml 3.11. Some people in the Coq development team are currently working on it. The basic idea is that the ML part of ssreflect will be compiled into a plugin (.cmxs) that will be dynamically loaded by Coq when needed. Cheers, -- Stéphane Glondu -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
