Library MetaCoq.Erasure.Extraction

Extraction setup for the erasure phase of template-coq.

Any extracted code planning to link with the plugin should use these same directives for consistency.

Extract Inductive Decimal.int ⇒ unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".

Extraction Blacklist config uGraph Universes Ast String List Nat Int
UnivSubst Typing Checker Retyping OrderedType Logic Common Equality Classes.

Extract Inductive Equations.Init.sigma ⇒ "(*)" ["(,)"].

Extract Constant PCUICTyping.fix_guard ⇒ "(fun x -> true)".
Extract Constant PCUICTyping.ind_guard ⇒ "(fun x -> true)".
Extract Constant PCUICSafeChecker.check_one_ind_body ⇒ "(fun _ _ _ _ _ _ _ -> ret envcheck_monad __)".

Cd "src".

Cd "..".