KM.extraction.Extraction

From KM Require Import PropQuantifiers Simp_env DecisionProcedure.

(* Simplified propositional quantifiers *)
Module Import S := Simp_env.S.
Module Import SPQr := PropQuant S.

Definition KM_E v f := Ef v f.
Definition KM_A v f := Af v f.

Definition KM_simp f := simp_form f.

Set Extraction Output Directory "extraction".

Separate Extraction Provable_dec KM_E KM_A KM_simp.