Checker_extraction.v 281 Bytes
Newer Older
1
Require Import Flover.CertificateChecker Flover.floverParser.
2
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
3

Heiko Becker's avatar
Heiko Becker committed
4
Extraction Language Ocaml.
5

6
Extraction "./binary/CoqChecker.ml" runChecker.