diff options
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. |