(* binders/ must be a subdirectory in the current working directory. *)  
Add LoadPath "binders".

Require Import Specif.
Require Import Metatheory.
Require Import cps_definitions_full.
Require Import cps_infrastructure_full.
Require Import cps_termination_full.

Set Extraction Optimize.
Set Extraction AutoInline.
Extraction Inline plus proj1_sig fst snd close_var close_var_spec_inf.


Extract Inductive bool => "bool" ["true" "false"].
Extract Inductive option => "option" ["Some" "None"].
Extract Constant eq_var_dec "a" "b" => "a=b".
Extraction Language Ocaml.
Extraction "cps_extracted" main.