.history
docs/_site
*.annot
.coq_config
*.cm*
*.vo
*.vok
*.vos
*.v.d
*.glob
Makefile.coq
Makefile.coq.conf
\#*#
*~
.*.aux
*.a
*.o
*.ml4.d
*.mllib.d
*.d
.merlin
html/*.html
.lia.cache
.hidden
_opam/
template-coq/Ascii.ml
template-coq/Ascii.mli
template-coq/Ast0.ml
template-coq/Ast0.mli
template-coq/AstUtils.ml
template-coq/AstUtils.mli
template-coq/Basics.ml
template-coq/Basics.mli
template-coq/BinInt.ml
template-coq/BinInt.mli
template-coq/BinNat.ml
template-coq/BinNat.mli
template-coq/BinNums.ml
template-coq/BinNums.mli
template-coq/BinPos.ml
template-coq/BinPos.mli
template-coq/BinPosDef.ml
template-coq/BinPosDef.mli
template-coq/Bool.ml
template-coq/Bool.mli
template-coq/Checker0.ml
template-coq/Checker0.mli
template-coq/config0.ml
template-coq/config0.mli
template-coq/Datatypes.ml
template-coq/Datatypes.mli
template-coq/DecidableType.ml
template-coq/DecidableType.mli
template-coq/Decimal.ml
template-coq/Decimal.mli
template-coq/Equalities.ml
template-coq/Equalities.mli
template-coq/FMapWeakList.ml
template-coq/FMapWeakList.mli
template-coq/FSetWeakList.ml
template-coq/FSetWeakList.mli
template-coq/Induction.ml
template-coq/Induction.mli
template-coq/LiftSubst.ml
template-coq/LiftSubst.mli
template-coq/List0.ml
template-coq/List0.mli
template-coq/Logic.ml
template-coq/Logic.mli
template-coq/MSetWeakList.ml
template-coq/MSetWeakList.mli
template-coq/Makefile.conf
template-coq/Nat0.ml
template-coq/Nat0.mli
template-coq/PeanoNat.ml
template-coq/PeanoNat.mli
template-coq/Specif.ml
template-coq/Specif.mli
template-coq/String0.ml
template-coq/String0.mli
template-coq/Typing0.ml
template-coq/Typing0.mli
template-coq/UnivSubst0.ml
template-coq/UnivSubst0.mli
template-coq/Wf.ml
template-coq/Wf.mli
template-coq/monad_utils.ml
template-coq/monad_utils.mli
template-coq/uGraph0.ml
template-coq/uGraph0.mli
template-coq/universes0.ml
template-coq/universes0.mli
template-coq/utils.ml
template-coq/utils.mli

checker/src/ascii.ml
checker/src/ascii.mli
checker/src/ast0.ml
checker/src/ast0.mli
checker/src/astUtils.ml
checker/src/astUtils.mli
checker/src/basics.ml
checker/src/basics.mli
checker/src/binInt.ml
checker/src/binInt.mli
checker/src/binNat.ml
checker/src/binNat.mli
checker/src/binNums.ml
checker/src/binNums.mli
checker/src/binPos.ml
checker/src/binPos.mli
checker/src/binPosDef.ml
checker/src/binPosDef.mli
checker/src/bool.ml
checker/src/bool.mli
checker/src/checker0.ml
checker/src/checker0.mli
checker/src/config0.ml
checker/src/config0.mli
checker/src/datatypes.ml
checker/src/datatypes.mli
checker/src/decidableType.ml
checker/src/decidableType.mli
checker/src/decimal.ml
checker/src/decimal.mli
checker/src/equalities.ml
checker/src/equalities.mli
checker/src/fMapWeakList.ml
checker/src/fMapWeakList.mli
checker/src/fSetWeakList.ml
checker/src/fSetWeakList.mli
checker/src/induction.ml
checker/src/induction.mli
checker/src/liftSubst.ml
checker/src/liftSubst.mli
checker/src/list0.ml
checker/src/list0.mli
checker/src/logic.ml
checker/src/logic.mli
checker/src/mSetWeakList.ml
checker/src/mSetWeakList.mli
checker/src/monad_utils.ml
checker/src/monad_utils.mli
checker/src/templateMonad.ml
checker/src/templateMonad.mli
checker/src/nat0.ml
checker/src/nat0.mli
checker/src/peanoNat.ml
checker/src/peanoNat.mli
checker/src/specif.ml
checker/src/specif.mli
checker/src/string0.ml
checker/src/string0.mli
checker/src/typing0.ml
checker/src/typing0.mli
checker/src/uGraph0.ml
checker/src/uGraph0.mli
checker/src/universes0.ml
checker/src/universes0.mli
checker/src/univSubst0.ml
checker/src/univSubst0.mli
checker/src/utils.ml
checker/src/utils.mli
checker/src/wf.ml
checker/src/wf.mli
/checker/src/retyping0.mli
/checker/src/retyping0.ml
/erasure/Makefile.conf
/erasure/Makefile.extraction
/erasure/Makefile.extraction.conf
/erasure/Makefile.plugin
/erasure/Makefile.plugin.conf
/erasure/src/eAst.ml
/erasure/src/eAst.mli
/erasure/src/extract.ml
/erasure/src/extract.mli
/erasure/src/eInduction.ml
/erasure/src/eInduction.mli
/erasure/src/eLiftSubst.ml
/erasure/src/eLiftSubst.mli
/erasure/src/eTtyping.ml
/erasure/src/eTyping.mli
/erasure/src/eUnivSubst.ml
/erasure/src/eUnivSubst.mli
/checker/Makefile.conf
/checker/src/ordersTac.mli
/checker/src/orderedType0.ml
/checker/src/orderedType0.mli
/checker/src/orders.ml
/checker/src/orders.mli
/checker/src/ordersTac.ml
/pcuic/Makefile.conf
/pcuic/src/templateToPCUIC.mli
/pcuic/src/templateToPCUIC.ml
/pcuic/src/pCUICUnivSubst.mli
/pcuic/src/pCUICUnivSubst.ml
/pcuic/src/pCUICTyping.mli
/pcuic/src/pCUICTyping.ml
/pcuic/src/pCUICLiftSubst.mli
/pcuic/src/pCUICLiftSubst.ml
/pcuic/src/pCUICAstUtils.mli
/pcuic/src/pCUICAstUtils.ml
/pcuic/src/pCUICAst.mli
/pcuic/src/pCUICAst.ml
/pcuic/Makefile.extraction
/pcuic/Makefile.extraction.conf
/pcuic/Makefile.pcuic
/pcuic/Makefile.pcuic.conf
/pcuic/Makefile.plugin
/pcuic/Makefile.plugin.conf
/erasure/src/eAstUtils.ml
/erasure/src/eAstUtils.mli
/erasure/src/eTyping.ml
/pcuic/src/pCUICChecker.ml
/pcuic/src/pCUICChecker.mli
/pcuic/src/pCUICRetyping.ml
/pcuic/src/pCUICRetyping.mli
/pcuic/src/templateToPCUIC.ml.rej
/pcuic/src/templateToPCUIC.mli.rej
/checker/src/basicAst.ml
/checker/src/basicAst.mli
/checker/src/typingWf.ml
/checker/src/typingWf.mli
/pcuic/src/pCUICSubstitution.ml
/pcuic/src/pCUICSubstitution.mli
/pcuic/src/pCUICWeakening.ml
/pcuic/src/pCUICWeakening.mli
/pcuic/src/pCUICWeakeningEnv.ml
/pcuic/src/pCUICWeakeningEnv.mli
/pcuic/src/pCUICNormal.ml
/pcuic/src/pCUICNormal.mli
/pcuic/src/pCUICPosition.ml
/pcuic/src/pCUICPosition.mli
/template-coq/theories/*.vio
/template-coq/theories/kernel/*.vio
/template-coq/theories/TemplateMonad/*.vio
/pcuic/src/logic0.mli
/pcuic/src/logic0.ml
/pcuic/src/logic.mli
/pcuic/src/logic.ml
/pcuic/src/init.mli
/pcuic/src/init.ml
/pcuic/src/classes0.mli
/pcuic/src/classes0.ml
/checker/metacoq-config
/translations/metacoq-config
/erasure/_CoqProject
/erasure/_PluginProject
/erasure/metacoq-config
/pcuic/_CoqProject
/pcuic/_PluginProject
/pcuic/metacoq-config
/checker/_CoqProject
/safechecker/metacoq-config
/safechecker/_PluginProject
/safechecker/_CoqProject
/safechecker/Makefile.safechecker.conf
/safechecker/Makefile.safechecker
/safechecker/Makefile.plugin.conf
/safechecker/Makefile.plugin
/pcuic/src/signature.ml
/pcuic/src/signature.mli
/template-coq/Makefile.template
/template-coq/Makefile.template.conf
/checker/_PluginProject
/checker/Makefile.plugin.conf
/checker/Makefile.plugin
/erasure/src/ssreflect.ml
/erasure/src/ssreflect.mli
/pcuic/src/PCUICInduction.ml
/pcuic/src/PCUICInduction.mli
/erasure/src/classes.ml
/erasure/src/classes.mli
/erasure/src/compare_dec.ml
/erasure/src/compare_dec.mli
/erasure/src/eqDecInstances.ml
/erasure/src/eqDecInstances.mli
/erasure/src/erasureFunction.ml
/erasure/src/erasureFunction.mli
/erasure/src/init.ml
/erasure/src/init.mli
/erasure/src/mSetList.ml
/erasure/src/mSetList.mli
/erasure/src/monad_utils.ml
/erasure/src/monad_utils.mli
/erasure/src/pCUICAst.ml
/erasure/src/pCUICAst.mli
/erasure/src/pCUICAstUtils.ml
/erasure/src/pCUICAstUtils.mli
/erasure/src/pCUICCumulativity.ml
/erasure/src/pCUICCumulativity.mli
/erasure/src/pCUICEquality.ml
/erasure/src/pCUICEquality.mli
/erasure/src/pCUICLiftSubst.ml
/erasure/src/pCUICLiftSubst.mli
/erasure/src/pCUICNormal.ml
/erasure/src/pCUICNormal.mli
/erasure/src/pCUICPosition.ml
/erasure/src/pCUICPosition.mli
/erasure/src/pCUICReflect.ml
/erasure/src/pCUICReflect.mli
/erasure/src/pCUICSafeChecker.ml
/erasure/src/pCUICSafeChecker.mli
/erasure/src/pCUICSafeConversion.ml
/erasure/src/pCUICSafeConversion.mli
/erasure/src/pCUICSafeLemmata.ml
/erasure/src/pCUICSafeLemmata.mli
/erasure/src/pCUICSafeReduce.ml
/erasure/src/pCUICSafeReduce.mli
/erasure/src/pCUICTyping.ml
/erasure/src/pCUICTyping.mli
/erasure/src/pCUICUnivSubst.ml
/erasure/src/pCUICUnivSubst.mli
/erasure/src/prelim.ml
/erasure/src/prelim.mli
/erasure/src/uGraph0.ml
/erasure/src/uGraph0.mli
/erasure/src/wGraph.ml
/erasure/src/wGraph.mli
/erasure/Makefile.erasure
/erasure/Makefile.erasure.conf
/erasure/src/classes0.ml
/erasure/src/classes0.mli
/erasure/src/erasure.ml
/erasure/src/erasure.mli
/erasure/src/templateToPCUIC.ml
/erasure/src/templateToPCUIC.mli
erasure/src/eqdepFacts.mli
erasure/src/eqdepFacts.ml
/erasure/src/ePretty.ml
/erasure/src/ePretty.mli
/pcuic/src/PCUICPretty.ml
/pcuic/src/PCUICPretty.mli
/pcuic/src/ssreflect.ml
pcuic/src/cMorphisms.ml
pcuic/src/cMorphisms.mli
pcuic/src/eqDecInstances.ml
pcuic/src/eqDecInstances.mli
pcuic/src/pCUICEquality.ml
pcuic/src/pCUICEquality.mli
pcuic/src/pCUICInduction.ml
pcuic/src/pCUICInduction.mli
pcuic/src/pCUICPretty.ml
pcuic/src/pCUICPretty.mli
pcuic/src/pCUICReflect.ml
pcuic/src/pCUICReflect.mli
pcuic/src/pCUICUtils.ml
pcuic/src/pCUICUtils.mli
erasure/src/pCUICReduction.ml
erasure/src/pCUICReduction.mli

/pcuic/src/ssreflect.mli
/_opam
/erasure/src/safeTemplateChecker.ml
/erasure/src/safeTemplateChecker.mli
/erasure/src/typing0.ml
/erasure/src/typing0.mli
/erasure/src/pCUICSafeRetyping.ml
/erasure/src/pCUICSafeRetyping.mli
erasure/src/pCUICInduction.ml
erasure/src/pCUICInduction.mli
erasure/src/mSetWeakList.ml
erasure/src/mSetWeakList.mli
erasure/src/utils.ml
erasure/src/utils.mli
erasure/src/ssrbool.ml
erasure/src/ssrbool.mli

template-coq/gen-src/cRelationClasses.mli.rej
.DS_Store

/translations/_CoqProject
test-suite/vs.mli
test-suite/vs.ml
test-suite/myMain.mli
test-suite/myMain.ml

template-coq/Makefile.plugin-e
template-coq/Makefile.template-e
template-coq/src/g_template_coq.ml
pcuic/Makefile.plugin-e
erasure/Makefile.plugin-e
safechecker/Makefile.plugin-e
erasure/src/g_metacoq_erasure.ml
erasure/src/pCUICChecker.ml
erasure/src/pCUICChecker.mli
erasure/src/pCUICPretty.ml
erasure/src/pCUICPretty.mli
erasure/src/byte.mli
erasure/src/byte.ml
myMain.ml
myMain.mli
vs.ml
vs.mli
*.v.timing
time-of-build.log
time-of-build-pretty.log
_build/**
extraction/src/*.ml
extraction/src/*.mli
erasure/src/orderedTypeAlt.ml
erasure/src/orderedTypeAlt.mli
erasure/src/orderedTypeEx.ml
erasure/src/orderedTypeEx.mli
erasure/src/kernames.ml
erasure/src/kernames.mli
erasure/src/reflect.ml
erasure/src/reflect.mli
erasure/src/pCUICWfUniverses.ml
erasure/src/pCUICWfUniverses.mli
erasure/src/signature.ml
erasure/src/signature.mli
erasure/src/eOptimizePropDiscr.ml
erasure/src/eOptimizePropDiscr.mli
erasure/src/pCUICErrors.ml
erasure/src/pCUICErrors.mli
erasure/src/pCUICTypeChecker.ml
erasure/src/pCUICTypeChecker.mli
erasure/src/pCUICPrimitive.ml
erasure/src/pCUICPrimitive.mli
erasure/src/pCUICCases.ml
erasure/src/pCUICCases.mli
template-coq/gen-src/specFloat.ml.rej

dependency-graph/