Checker_extraction.v 278 Bytes
Newer Older
1 2
Require Import Daisy.CertificateChecker Daisy.daisyParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
3 4 5

Extraction Language Ocaml.

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