Library MetaCoq.Template.Extraction

Extraction setup for template-coq.

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

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

Extract Constant utils.ascii_compare ⇒
"fun x y -> match Char.compare x y with 0 -> Eq | x when x < 0 -> Lt | _ -> Gt".

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

Cd "gen-src".

Recursive Extraction Library Extractable.
Extraction Library Induction.
Extraction Library LiftSubst.
Extraction Library UnivSubst.
Extraction Library Pretty.
Extraction Library config.

Cd "..".