diff --git a/docs/.gitignore b/docs/.gitignore
index b0c520f6f1f62474548cbe8f27ad3630551ea5a0..7969c4f55c81e769b2facb814aa4d2e95e681c84 100644
--- a/docs/.gitignore
+++ b/docs/.gitignore
@@ -10,3 +10,5 @@
 *.blg
 *.bcf
 *.run.xml
+_*_.tex
+auto/*.el
diff --git a/docs/iris/algebra.tex b/docs/algebra.tex
similarity index 100%
rename from docs/iris/algebra.tex
rename to docs/algebra.tex
diff --git a/docs/iris/constructions.tex b/docs/constructions.tex
similarity index 100%
rename from docs/iris/constructions.tex
rename to docs/constructions.tex
diff --git a/docs/iris/derived.tex b/docs/derived.tex
similarity index 100%
rename from docs/iris/derived.tex
rename to docs/derived.tex
diff --git a/docs/iris/encodings.tex b/docs/encodings.tex
similarity index 100%
rename from docs/iris/encodings.tex
rename to docs/encodings.tex
diff --git a/docs/iris/iris.tex b/docs/iris.tex
similarity index 100%
rename from docs/iris/iris.tex
rename to docs/iris.tex
diff --git a/docs/iris/bib.bib b/docs/iris/bib.bib
deleted file mode 120000
index 8b7cbf87be88dfca92040a7222aa88e397178620..0000000000000000000000000000000000000000
--- a/docs/iris/bib.bib
+++ /dev/null
@@ -1 +0,0 @@
-../bib.bib
\ No newline at end of file
diff --git a/docs/iris/listproc.sty b/docs/iris/listproc.sty
deleted file mode 120000
index 7c5b7f009564ed54ac2302e55e70730bda96e97c..0000000000000000000000000000000000000000
--- a/docs/iris/listproc.sty
+++ /dev/null
@@ -1 +0,0 @@
-../listproc.sty
\ No newline at end of file
diff --git a/docs/iris/locallabel.sty b/docs/iris/locallabel.sty
deleted file mode 120000
index b5cf8440324e58c71982b2b53aff9a1f54b01822..0000000000000000000000000000000000000000
--- a/docs/iris/locallabel.sty
+++ /dev/null
@@ -1 +0,0 @@
-../locallabel.sty
\ No newline at end of file
diff --git a/docs/iris/mathpartir.sty b/docs/iris/mathpartir.sty
deleted file mode 120000
index 882eef9e39db25828dccb87e6f655b55d290f2ae..0000000000000000000000000000000000000000
--- a/docs/iris/mathpartir.sty
+++ /dev/null
@@ -1 +0,0 @@
-../mathpartir.sty
\ No newline at end of file
diff --git a/docs/iris/pftools.sty b/docs/iris/pftools.sty
deleted file mode 120000
index 68af43890729738796dffd18fdd3dadbf601495b..0000000000000000000000000000000000000000
--- a/docs/iris/pftools.sty
+++ /dev/null
@@ -1 +0,0 @@
-../pftools.sty
\ No newline at end of file
diff --git a/docs/iris/setup.tex b/docs/iris/setup.tex
deleted file mode 120000
index 7a0f2491cb5a519dc1909df6ef55a74fd0a1b039..0000000000000000000000000000000000000000
--- a/docs/iris/setup.tex
+++ /dev/null
@@ -1 +0,0 @@
-../setup.tex
\ No newline at end of file
diff --git a/docs/iris/logic.tex b/docs/logic.tex
similarity index 96%
rename from docs/iris/logic.tex
rename to docs/logic.tex
index 2283fc838793d6425847411b6ea3c72cb75a7356..6f9293703dd1d6efb754f4ebb565fa8bff5519ab 100644
--- a/docs/iris/logic.tex
+++ b/docs/logic.tex
@@ -1,18 +1,3 @@
-% CONVENTION:
-%	Use \Ra/Lra for the logic and \implies/\iff for the metalogic.
-
-% This short (for now) note lays out a \emph{generic} separation logic which
-% manages sharing through invariants and ownership through (partial commutative)
-% monoids.  The logic is generic in that the actual language it applies to is
-% taken as a parameter, giving in particular the atomic (per-thread) reduction
-% relation.  Over this, we layer concurrency (by giving a semantics to \kw{fork}
-% and lifting to thread pools).  The generic logic provides numerous logical
-% connectives and the semantics of Hoare triples and view shifts, together with a
-% large portion of the proof theory---including, in particular, the structural
-% rules for Hoare logic.  Ultimately, these are proved sound relative to some
-% simple assumptions about the language.  It should be possible, moreover, to give
-% a generic adequacy proof for Hoare triples as applied to the lifted thread-pool
-% semantics.
 
 \section{Parameters to the logic}
 
diff --git a/docs/iris/model.tex b/docs/model.tex
similarity index 100%
rename from docs/iris/model.tex
rename to docs/model.tex
diff --git a/docs/setup.tex b/docs/setup.tex
index 5ba0f0f2009666a8079fc745dde7f71f51c5715b..22e824e6b8ba340f3d675a026a19f6136df86f37 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -277,7 +277,7 @@
 %% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\Sig}{\Sigma}
+\newcommand{\Sig}{\mathcal{S}}
 \newcommand{\SigType}{\mathcal{T}}
 \newcommand{\SigFn}{\mathcal{F}}
 \newcommand{\sigfn}{F}
@@ -292,7 +292,7 @@
 \newcommand{\termB}{u}
 \newcommand{\termVal}{V}
 
-\newcommand{\sort}{\sigma}
+\newcommand{\sort}{\Sigma}
 
 \newcommand{\vctx}{\Gamma}
 \newcommand{\pfctx}{\Theta}
@@ -463,3 +463,8 @@
 
 \newcommand{\AuthInv}{\textsf{AuthInv}}
 \newcommand{\Auth}{\textsf{Auth}}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End: