*.annot
.coq_config
*.cm*
*.vo
*.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
/extraction/Makefile.conf
/extraction/Makefile.extraction
/extraction/Makefile.extraction.conf
/extraction/Makefile.plugin
/extraction/Makefile.plugin.conf
/extraction/src/eAst.ml
/extraction/src/eAst.mli
/extraction/src/extract.ml
/extraction/src/extract.mli
/extraction/src/eInduction.ml
/extraction/src/eInduction.mli
/extraction/src/eLiftSubst.ml
/extraction/src/eLiftSubst.mli
/extraction/src/eTtyping.ml
/extraction/src/eTyping.mli
/extraction/src/eUnivSubst.ml
/extraction/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
/extraction/src/eAstUtils.ml
/extraction/src/eAstUtils.mli
/extraction/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
/pcuic/src/pCUICMetaTheory.ml
/pcuic/src/pCUICMetaTheory.mli
/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
/extraction/_CoqProject
/extraction/_PluginProject
/extraction/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