Verified Extraction 0.9.1 for Coq 8.19

This preliminary version of the verified extraction plugin work with MetaCoq 1.3.1, Coq 8.19 and malfunction 0.6. It provides an alternative extraction procedure from Coq to OCaml through the untyped Malfunction language.

What's Changed

• Extraction plugin by @mattam82 in #1
• semantics with heap by @tabareau in #2
• complete proof that eval -> interpret by @tabareau in #4
• Pipeline theorem by @yforster in #6
• WIP on realizability semantics by @tabareau in #5
• Enable benchmarking, and others things by @yforster in #8
• complete pipeline up to admits by @tabareau in #9
• Metacoq bump by @mattam82 in #12
• Extract inductive implementation by @mattam82 in #14
• Fix and test bootstrapping and plugin feature (dynlink with coq) by @mattam82 in #15
• Support reification of computed results by @mattam82 in #16
• Unsafe flags by @mattam82 in #17
• Update metacoq commit by @mattam82 in #18
• Update to latest metacoq (typo fix) by @mattam82 in #19
• Rename "MetaCoq Extraction" to "Verified Extraction" everywhere by @mattam82 in #21
• Fix multiple function extraction by @yforster in #22
• Cleanup by @yforster in #23
• Cleanup directory structure by @yforster in #24
• Rename Malfunction.VerifiedPlugin.Loader into VerifiedExtraction.Extr… by @yforster in #25
• Fix several things suggested by AE reviewers by @yforster in #26

New Contributors

• @mattam82 made their first contribution in #1
• @tabareau made their first contribution in #2
• @yforster made their first contribution in #6

Full Changelog: https://github.com/yforster/coq-verified-extraction/commits/v0.9-8.19