Library MetaCoq.PCUIC.Extraction
Require Import MetaCoq.Template.utils.
Require Import FSets ssreflect ExtrOcamlBasic ExtrOcamlZInt.
Require Import FSets ssreflect ExtrOcamlBasic ExtrOcamlZInt.
Extraction setup for the pcuic phase of MetaCoq.
Extraction Blacklist Classes config uGraph universes Ast String List Logic Logic0 Nat Int
UnivSubst Typing Checker Retyping OrderedType Classes equality.
Set Warnings "-extraction-opaque-accessed".
Set Warnings "-extraction-reserved-identifier".
Cd "src".
Extraction Library Init.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICUnivSubst
PCUICInduction PCUICLiftSubst PCUICTyping PCUICNormal PCUICSafeLemmata
PCUICEquality
PCUICPretty TemplateToPCUIC.
From Equations Require Import Equations.
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 Inline MCEquality.transport.
Extraction Library Signature.
Extraction Library Classes.
Extraction Library ssreflect.
Extraction Library CMorphisms.
Extraction Library PCUICAst.
Extraction Library PCUICAstUtils.
Extraction Library PCUICUtils.
Extraction Library PCUICInduction.
Extraction Library PCUICUnivSubst.
Extraction Library PCUICLiftSubst.
Extraction Library PCUICReflect.
Extraction Library EqDecInstances.
Extraction Library PCUICEquality.
Extraction Library PCUICTyping.
Extraction Library TemplateToPCUIC.
Extraction Library PCUICPretty.
Cd "..".