Commit e38f76b0 authored by Robbert's avatar Robbert

Merge branch 'ralf/docs' into 'master'

move docs around

See merge request iris/iris!323
parents e8f260ef 14ac28b1
Pipeline #20795 passed with stage
in 15 minutes and 10 seconds
# Contributing to the Iris Coq Development
Here you can find some how-tos for various thing sthat might come up when doing
Iris development.
Iris development. This is for contributing to Iris itself; see
[the README]( for resources helpful for all Iris
## How to submit a merge request
This diff is collapsed.
......@@ -9,7 +9,7 @@ For using the Coq library, check out the
For understanding the theory of Iris, a LaTeX version of the core logic
definitions and some derived forms is available in
[docs/iris.tex](docs/iris.tex). A compiled PDF version of this document is
[docs/iris.tex](tex/iris.tex). A compiled PDF version of this document is
[available online](
## Building Iris
......@@ -83,7 +83,7 @@ followed by `make build-dep`.
[MoSeL](, which extends Coq with contexts for
intuitionistic and spatial BI++ assertions. It also contains tactics for
interactive proofs. Documentation can be found in
* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
* The subfolder [lib](theories/heap_lang/lib) contains a few derived
......@@ -113,11 +113,11 @@ that should be compatible with this version:
Getting along with Iris in Coq:
* Iris proof patterns are documented in the [proof guide](
* Syntactic conventions are described in the [style guide](
* Iris proof patterns are documented in the [proof guide](docs/
* Syntactic conventions are described in the [style guide](docs/
* The Iris tactics are described in the
[the Iris Proof Mode (IPM) / MoSeL documentation]( as well as the
[HeapLang documentation](
[the Iris Proof Mode (IPM) / MoSeL documentation](docs/ as well as the
[HeapLang documentation](docs/
* The generated coqdoc is [available online](
Contacting the developers:
......@@ -137,7 +137,7 @@ Contacting the developers:
* Information on how to set up your editor for unicode input and output is
collected in [](
collected in [](docs/
* If you are writing a paper that uses Iris in one way or another, you could use
the [Iris LaTeX macros](docs/iris.sty) for typesetting the various Iris
the [Iris LaTeX macros](tex/iris.sty) for typesetting the various Iris
This diff is collapsed.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment