Commit 5f230480 authored by Heiko Becker's avatar Heiko Becker

Merge remote-tracking branch 'origin/master' into affine_arithmetic

parents 9421bbb5 3901659c
Require Import Flover.CertificateChecker Flover.floverParser.
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.
\ No newline at end of file
......@@ -14,7 +14,7 @@ Module OWL.
Proof.
now unfold eq; split; subst.
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).
Proof.
......@@ -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).
Check (forall x S, x S -- {{x}}).
Lemma not_in_not_mem:
forall n S,
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:
ocamlc -c big.ml
ocamlc -c CoqChecker.ml
ocamlc -c CoqChecker.mli
ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
all: native
Subproject commit c25dae0a1ede617a25e49162f6f47ac9a1a2381a
Subproject commit b801379405021120d0dd2b8d3a3a886c84a114a4
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