summaryrefslogtreecommitdiffstats
path: root/.gitignore
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-08-28 19:37:02 +0200
committerThomas Letan <lthms@soap.coffee>2020-08-28 20:10:04 +0200
commita7e45316109aa220bd7be9da0888dfbbf86e6aec (patch)
treeba613dc8a8abe396d209e75fc49d7897bee3349b /.gitignore
parentAdd a page to display my keystrokes reporting (diff)
Heavy reworking of the Ltac series
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore4
1 files changed, 3 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index cb12f58..002b3cc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -33,10 +33,11 @@ build.log
.lia.cache
site/posts/AlgebraicDatatypes.html
site/posts/StronglySpecifiedFunctionsProgram.html
+site/posts/LtacPatternMatching.html
site/posts/ClightIntroduction.html
site/posts/StronglySpecifiedFunctions.html
site/posts/RewritingInCoq.html
-site/posts/Ltac101.html
+site/posts/LtacMetaprogramming.html
site/posts/MixingLtacAndGallina.html
site/index.html
site/news/ColorlessThemes-0.2.html
@@ -51,6 +52,7 @@ site/posts/DiscoveringCommonLisp.html
site/posts/ExtensibleTypeSafeErrorHandling.html
site/posts/MonadTransformers.html
site/posts/CleopatraV1.html
+site/posts/Ltac.html
build/
site/style/main.css
# end generated files