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

5
Extraction Language OCaml.
6

7
(*
8
Extraction "./binary/CoqChecker.ml" runChecker.
9
*)