coqutil: coinductive version of always · mit-plv/rupicola@2aa6b13

Commit

coqutil: coinductive version of always

Browse files

andres-erbsen committed Apr 2, 2024

1 parent 7259f52 commit 2aa6b13

+75 −0		LiveVerif/src/LiveVerifExamples/bsearch.v
+39 −0		LiveVerif/src/LiveVerifExamples/memcpy.v
+170 −0		LiveVerif/src/LiveVerifExamples/mini_stagefright.v
+26 −0		compiler/src/compiler/CompilerInvariant.v
+189 −0		compiler/src/compiler/ElfPrinter.v
+1 −1		deps/coqutil