Commits · f0f9f3b67ec5a40ac51f4c8d8df23be89bc4913c · Pierre Roux / Iris

Nov 12, 2020
- add prelude to readme (and fix a bunch of links while we are at it) · 7b99b90e
  Ralf Jung authored 4 years ago
  
  7b99b90e
Nov 10, 2020
- address feedback · 8695972d
  Ralf Jung authored 4 years ago
  
  8695972d
- Apply 2 suggestion(s) to 1 file(s) · c568ece0
  Ralf Jung authored 4 years ago
  
  c568ece0
- remove outdated 'm' metavaraibe; enable coq syntax highlighting · 3cd45dbc
  Ralf Jung authored 4 years ago
  
  3cd45dbc
- add docs and changelog entry · 0e228686
  Ralf Jung authored 4 years ago
  
  0e228686
Nov 06, 2020
- editing of equalities documentation · b85bebc3
  Ralf Jung authored 4 years ago
  
  b85bebc3
- split RA docs into separate file, and general doc updates · 8cfe4ceb
  Ralf Jung authored 4 years ago
  
  8cfe4ceb
- Documentation on Iris equalities · d8e8dfea
  Paolo G. Giarrusso authored 5 years ago and Ralf Jung committed 4 years ago
  
  d8e8dfea
Oct 29, 2020
- Fix typos · 07d25e67
  Yusuke Matsushita authored 4 years ago and Robbert Krebbers committed 4 years ago
  
  07d25e67
Sep 29, 2020
- Improve docs for `iModIntro`. · ceb9fa1f
  Robbert Krebbers authored 4 years ago
  
  Based om iris/iris!467 (comment 53064) by @Blaisorblade.
  ceb9fa1f
Jul 15, 2020
- Unicode is required in Iris itself · 04d223b9
  Ralf Jung authored 4 years ago
  
  04d223b9
Jul 04, 2020
- mention that the ASCII syntax exists (but we recommend unicode) · 7eaf255d
  Ralf Jung authored 4 years ago
  
  7eaf255d
Jun 29, 2020
- Fix typos in docs of `iNext`. · 462b056f
  Robbert Krebbers authored 4 years ago
  
  462b056f
May 22, 2020
- More documentation on `done`. · 73c3a5ed
  Robbert Krebbers authored 4 years ago
  
  73c3a5ed
Apr 07, 2020
- Apply suggestion to docs/proof_mode.md · d5b00af7
  Robbert Krebbers authored 4 years ago
  
  d5b00af7
- Remark about space. · 34062842
  Robbert Krebbers authored 4 years ago
  
  34062842
- Document `%H` pattern. · 7b1c37df
  Robbert Krebbers authored 4 years ago
  
  This closes issue #305.
  7b1c37df
Mar 27, 2020
- Spell check proof_guide.md · 3945e6bb
  Paolo G. Giarrusso authored 5 years ago
  
  3945e6bb
Mar 21, 2020
- Add VS code to the editor.md docs · b32af454
  Jules Jacobs authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  b32af454
Mar 20, 2020
- Add documentation. · ba3f6ce2
  Robbert Krebbers authored 5 years ago
  
  ba3f6ce2
Feb 26, 2020
- slightly expand notation docs · af197fa4
  Ralf Jung authored 5 years ago
  
  af197fa4
- merge proof_guide and style_guide · b544d65d
  Ralf Jung authored 5 years ago
  
  b544d65d
- Add documentation. Thanks to @Blaisorblade . · 62d5e8b5
  Robbert Krebbers authored 5 years ago
  
  62d5e8b5
- Fix typo. · a0e0e916
  Robbert Krebbers authored 5 years ago
  
  a0e0e916
Feb 18, 2020
- Remove more new lines. · 00bd9cf1
  Robbert Krebbers authored 5 years ago
  
  00bd9cf1
- And more useless new lines. · 461c88d6
  Robbert Krebbers authored 5 years ago
  
  461c88d6
- Remove useless newlines in `proof_mode.md`. · 1a5d7d58
  Robbert Krebbers authored 5 years ago
  
  1a5d7d58
- Add proof mode documentation for the `-# pat` intro pattern. · 226b8579
  Robbert Krebbers authored 5 years ago
  
  226b8579
- Improve docs of the `# pat` intro pattern. · 25061957
  Robbert Krebbers authored 5 years ago
  
  25061957
Feb 06, 2020
- Document CoqIDE Unicode binding configuration · 23b2362a
  Tej Chajed authored 5 years ago and Robbert Krebbers committed 5 years ago
  
  Fixes #269.
  23b2362a
Dec 19, 2019
- [doc] Fix links to doc files · d5763982
  Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago
  
  d5763982
Dec 14, 2019
- [doc] Copy edit the heap lang documentation · 6385b7ea
  Tej Chajed authored 5 years ago
  
  6385b7ea
Nov 10, 2019
- CAS -> CmpXchg in HeapLang tactic docs · 86a8269d
  Paolo G. Giarrusso authored 5 years ago
  
  86a8269d
Nov 01, 2019
- move docs around · 14ac28b1
  Ralf Jung authored 5 years ago
  
  14ac28b1
Oct 05, 2019
- fixed some proof formatting errors · 0a151fd4
  Derek Dreyer authored 5 years ago
  
  0a151fd4
Aug 30, 2019
- fix typo · a0b4ccc2
  Dan Frumin authored 5 years ago
  
  a0b4ccc2
Jun 14, 2019
- make variable names a bit more consistent between Coq and LaTeX · ce20ffb1
  Ralf Jung authored 5 years ago
  
  ce20ffb1
- temporary link to prophecy MR, until we can reference a paper instead · 8f443ec0
  Ralf Jung authored 5 years ago
  
  8f443ec0
- note that observations are observable events · e262cd8e
  Ralf Jung authored 5 years ago
  
  e262cd8e
- docs: fix typo · 4f526c98
  Ralf Jung authored 5 years ago
  
  4f526c98