_CoqConfig

-Q theories MirrorCore
-Q examples McExamples

-I src
-I $(COQLIB)/user-contrib/PluginUtils

src/reify_Core.mli
src/reify_Core.ml
src/reify_Monad.ml
src/reify_Lambda_shell.ml4
src/reify_Lambda_plugin.mllib

theories/ExprI.v
theories/CtxLogic.v
theories/TypesI.v
theories/EnvI.v
theories/OpenT.v
theories/Generic.v
theories/SubstituteI.v
theories/VariablesI.v
theories/AbsAppI.v
theories/UnifyI.v
theories/ExprProp.v
theories/ExprSem.v
theories/ExprDAs.v
theories/SymI.v
theories/SubstI.v
theories/Instantiate.v
theories/VarsToUVars.v
theories/Lemma.v
theories/PLemma.v
theories/LemmaApply.v
theories/Simple.v
theories/Polymorphic.v

theories/Subst/UVarMap.v
theories/Subst/FMapSubst.v

theories/CTypes/CoreTypes.v
theories/CTypes/GenericTypes.v
theories/CTypes/TSyms.v
theories/CTypes/TSymOneOf.v
theories/CTypes/ProdType.v
theories/CTypes/ListType.v
theories/CTypes/BaseType.v
theories/CTypes/CTypeUnify.v

theories/Util/Approx.v
theories/Util/Iteration.v
theories/Util/ListMapT.v
theories/Util/Forwardy.v
theories/Util/Quant.v
theories/Util/Nat.v
theories/Util/HListBuild.v
theories/Util/Compat.v
theories/Util/SemiDec.v

theories/syms/SymEnv.v
theories/syms/SymPolyEnv.v
theories/syms/SymSum.v
theories/syms/SymProd.v
theories/syms/SymOneOf.v
theories/syms/SymSimple.v

theories/Lambda/ExprCore.v
theories/Lambda/ExprDI.v
theories/Lambda/ExprDsimul.v
theories/Lambda/ExprD.v
theories/Lambda/ExprDFacts.v
theories/Lambda/ExprTac.v
theories/Lambda/Expr.v
theories/Lambda/ExprLift.v
theories/Lambda/Red.v
theories/Lambda/RedAll.v
theories/Lambda/TypedFoldEager.v
theories/Lambda/TypedFoldLazy.v
theories/Lambda/TypedFoldApp.v
theories/Lambda/FoldApp.v
theories/Lambda/StrongFoldApp.v
theories/Lambda/Lemma.v
theories/Lambda/ExprUnify_common.v
theories/Lambda/ExprUnify_simple.v
theories/Lambda/ExprUnify_simul.v
theories/Lambda/ExprUnify.v
theories/Lambda/ExprSubst.v
theories/Lambda/ExprSubstitute.v
theories/Lambda/AppN.v
theories/Lambda/ExprVariables.v
theories/Lambda/RewriteRelations.v
theories/Lambda/Ptrns.v
theories/Lambda/Rtac.v
theories/Lambda/Reify.v
theories/Lambda/PolyInst.v
theories/Lambda/RewriteStrat.v
theories/Lambda/Rewrite/Core.v
theories/Lambda/Rewrite/BottomUp.v
theories/Lambda/Rewrite/Tactic.v
theories/Lambda/Rewrite/Repeat.v
theories/Lambda/Rewrite/Reduce.v
theories/Lambda/Rewrite/Respectful.v
theories/Lambda/Rewrite/Rewrite.v
theories/Lambda/Rewrite/HintDbs.v

theories/Views/View.v
theories/Views/TypeView.v
theories/Views/FuncView.v
theories/Views/Ptrns.v
theories/Views/Ptrns2.v
theories/Views/ViewSum.v
theories/Views/ViewSumN.v

theories/Lib/ListView.v
theories/Lib/NatView.v
theories/Lib/StringView.v
theories/Lib/BoolView.v
theories/Lib/ProdView.v
theories/Lib/ApplicativeView.v
theories/Lib/EqView.v
theories/Lib/ListOpView.v

theories/RTac/BIMap.v
theories/RTac/Ctx.v
theories/RTac/Core.v
theories/RTac/CoreK.v
theories/RTac/IsSolved.v
theories/RTac/PApply.v
theories/RTac/SpecLemmas.v
theories/RTac/RunOnGoals.v
theories/RTac/RunOnGoals_list.v
theories/RTac/Then.v
theories/RTac/Try.v
theories/RTac/Repeat.v
theories/RTac/Rec.v
theories/RTac/Idtac.v
theories/RTac/First.v
theories/RTac/Fail.v
theories/RTac/Solve.v
theories/RTac/SolveK.v
theories/RTac/ThenK.v
theories/RTac/IdtacK.v
theories/RTac/runTacK.v
theories/RTac/Assumption.v
theories/RTac/Intro.v
theories/RTac/Apply.v
theories/RTac/EApply.v
theories/RTac/Simplify.v
theories/RTac/Instantiate.v
theories/RTac/Minify.v
theories/RTac/AtGoal.v
theories/RTac/Reduce.v
theories/RTac/Interface.v
theories/RTac/Auto.v
theories/RTac/RTac.v

theories/Reify/Patterns.v
theories/Reify/Reify.v
theories/Reify/ReifyClass.v
theories/Reify/ReifyView.v

examples/Tauto/MSimpleTyp.v
examples/Tauto/ILogic.v
examples/Tauto/ILogicFunc.v
examples/Tauto/ILogicReify.v
examples/Tauto/Tauto.v
examples/Tauto/LtacDemo.v
examples/Tauto/RtacDemo.v

examples/Cancel/Monoid.v
examples/Cancel/MonoidSyntaxSimple.v
examples/Cancel/MonoidSyntaxNoDec.v
examples/Cancel/MonoidSyntaxWithConst.v
examples/Cancel/MonoidSyntaxModular.v
examples/Cancel/LtacDemo.v
examples/Cancel/RtacDemo.v

examples/Hoare/ILogic.v
examples/Hoare/ILogicFunc.v
examples/Hoare/LogicTac.v
examples/Hoare/Imp.v
examples/Hoare/ImpMetaTheory.v
examples/Hoare/ImpSyntax.v
examples/Hoare/Verify.v
examples/Hoare/Tests.v

# examples/Simple/Simple.v
# examples/Simple/SimpleReify.v
# examples/Simple/SimpleExt.v
# examples/Simple/FoldTest.v

# examples/Reify/ModularReify.v

# examples/RTac/Demo.v

examples/PolyRewrite/MSimple.v
examples/PolyRewrite/MSimpleReify.v

examples/PolyRewrite/QuantifierPuller/PolyQuantPullRtac.v
examples/PolyRewrite/QuantifierPuller/RtacDemo.v
examples/PolyRewrite/QuantifierPuller/LtacDemo.v

examples/PolyApply/MSimpleType.v
examples/PolyApply/MSimpleFunc.v
examples/PolyApply/DemoPolyApply.v

examples/PolyRewrite/Monads/Monad.v
examples/PolyRewrite/Monads/LtacDemo.v
examples/PolyRewrite/Monads/RtacDemo.v
examples/PolyRewrite/Monads/MSimpleMonads.v
examples/PolyRewrite/Monads/MSimpleMonadsReify.v