Commit 3901659c authored by Heiko Becker's avatar Heiko Becker

Compatibility, fix binary compilation

parent f1785f18
Require Import Flover.CertificateChecker Flover.floverParser. Require Import Flover.CertificateChecker Flover.floverParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt. Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Extraction Language Ocaml. Extraction Language OCaml.
Extraction "./binary/CoqChecker.ml" runChecker. Extraction "./binary/CoqChecker.ml" runChecker.
\ No newline at end of file
...@@ -14,7 +14,7 @@ Module OWL. ...@@ -14,7 +14,7 @@ Module OWL.
Proof. Proof.
now unfold eq; split; subst. now unfold eq; split; subst.
Qed. Qed.
Definition compare := Compare_dec.nat_compare. Definition compare := Nat.compare.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
Proof. Proof.
...@@ -42,8 +42,6 @@ Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity). ...@@ -42,8 +42,6 @@ Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity).
Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity). Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity).
Check (forall x S, x S -- {{x}}).
Lemma not_in_not_mem: Lemma not_in_not_mem:
forall n S, forall n S,
NatSet.mem n S = false -> NatSet.mem n S = false ->
......
#bytes:
# ocamlc -c CoqChecker.ml
# ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml
native: native:
ocamlc -c big.ml ocamlc -c big.ml
ocamlc -c CoqChecker.ml ocamlc -c CoqChecker.ml
ocamlc -c CoqChecker.mli
ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
all: native all: native
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment