Library MetaCoq.PCUIC.Extraction

Extraction setup for the pcuic phase of MetaCoq.

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)".

Extraction Blacklist config uGraph universes Ast String List Logic Logic0 Nat Int
UnivSubst Typing Checker Retyping OrderedType Classes equality.

Cd "src".

Extraction Library Init.

Extraction Inline Equations.Prop.Classes.noConfusion.
Extraction Inline Equations.Prop.Logic.eq_elim.
Extraction Inline Equations.Prop.Logic.eq_elim_r.
Extraction Inline Equations.Prop.Logic.transport.
Extraction Inline Equations.Prop.Logic.transport_r.
Extraction Inline Equations.Prop.Logic.False_rect_dep.
Extraction Inline Equations.Prop.Logic.True_rect_dep.
Extraction Inline Equations.Init.pr1.
Extraction Inline Equations.Init.pr2.
Extraction Inline Equations.Init.hidebody.
Extraction Inline Equations.Prop.DepElim.solution_left.

Extraction Library Signature.
Extraction Library Classes.
Extraction Library ssreflect.
Extraction Library CMorphisms.
Extraction Library PCUICAst.
Extraction Library PCUICAstUtils.
Extraction Library PCUICInduction.
Extraction Library PCUICUnivSubst.
Extraction Library PCUICLiftSubst.
Extraction Library PCUICReflect.
Extraction Library EqDecInstances.
Extraction Library PCUICEquality.
Extraction Library PCUICTyping.
Extraction Library PCUICChecker.
Extraction Library PCUICRetyping.
Extraction Library PCUICMetaTheory.
Extraction Library TemplateToPCUIC.
Extraction Library PCUICPretty.
Cd "..".