> On Feb 11, 2016, at 11:36 AM, Yozo TODA <yozo.t...@gmail.com> wrote: > > (my provider is treated as a SPAM source by UCEProtect. > now I'm trying to send this message from gmail...) > > Daniel Dickman writes: > ...... >> Please don't commit this until I have time to verify with compcert. > > Daniel, how's your working?
please see http://marc.info/?l=openbsd-ports&m=145460329517278&w=2 > I didn't try Compcert and not sure if Compcert is compliant to coq 8.5, > how about branching math/coq to math/coq/8.4 and math/coq/8.5 ? I'd be against doing this. > > -- yozo. >
