diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 15:11:48 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 15:11:48 +0200 |
| commit | 322f3c865341fdfd5d22ab885b2934a5213ddbaa (patch) | |
| tree | 70912af2a6cd75d72b57172d910d71a6abd2d447 /extraction | |
| parent | 6b87278c399332f67a4b40958ea2386bb3c1c66e (diff) | |
| download | compcert-kvx-322f3c865341fdfd5d22ab885b2934a5213ddbaa.tar.gz compcert-kvx-322f3c865341fdfd5d22ab885b2934a5213ddbaa.zip | |
Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy
Inline directives in extraction.v make the Caml output efficient and almost nice.
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index aecc07a5..8e13264c 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -12,6 +12,7 @@ Require Coqlib. Require Wfsimpl. +Require DecidableClass Decidableplus. Require AST. Require Iteration. Require Floats. @@ -39,6 +40,12 @@ Require Import ExtrOcamlString. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". +(* Decidable *) + +Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide + Decidableplus.Decidable_and Decidableplus.Decidable_or + Decidableplus.Decidable_not Decidableplus.Decidable_implies. + (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. |