One way I'd do this is adding a subdir at the top
$ ls FlocqExtern/IEEE754
BinarySingleNan.v Binary.v
and try to spoof the patterns in Flocq.IEEE754.Binary{SingleNaN,}.v
Once Bmax is vendored that way (and coq_makefile/_CoqProject are caught up), follow the patterns in IEEE754_extras.v appending Bmax and proofs.
Would yall have a preferred design @ak-2485 @andrew-appel ? or does this sound reasonable?
One way I'd do this is adding a subdir at the top
and try to spoof the patterns in
Flocq.IEEE754.Binary{SingleNaN,}.vOnce
Bmaxis vendored that way (andcoq_makefile/_CoqProjectare caught up), follow the patterns inIEEE754_extras.vappendingBmaxand proofs.Would yall have a preferred design @ak-2485 @andrew-appel ? or does this sound reasonable?