1. 29 Nov, 2017 5 commits
    • David Swasey's avatar
      Reserve more notation in `integers.v`. · fffa7c44
      David Swasey authored
      Avoid duplicating details like `at level 35`.
      
      This is a bit of a slippery slope. (I reserved just the notation that
      I overload elsewhere.)
      fffa7c44
    • Robbert's avatar
      Merge branch 'ssrfun' into 'master' · 735e4e4d
      Robbert authored
      Make x.1, x.2 notation compatible with ssrfun.
      
      See merge request robbertkrebbers/coq-stdpp!21
      735e4e4d
    • David Swasey's avatar
      Make x.1, x.2 notation compatible with ssrfun. · 5c069266
      David Swasey authored
      Enable one to import both stdpp's base and ssrfun.
      
      Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
      (This change affects one proof in Iris.)
      5c069266
    • Ralf Jung's avatar
      Merge branch 'ralf/opam' into 'master' · 2b35253e
      Ralf Jung authored
      Allow compiling against "dev" version of Coq
      
      See merge request robbertkrebbers/coq-stdpp!20
      2b35253e
    • Ralf Jung's avatar
      Allow compiling against "dev" version of Coq · a5bc9446
      Ralf Jung authored
      This matches e.g. Iris allowing a "dev" version of std++: You can install a
      "dev" version to test stuff, but then you are responsible for making sure that
      these versions actually work together.  We rely on that when testing things
      against Iris master every night, for which purpose we install Iris master as
      "dev" version.
      a5bc9446
  2. 28 Nov, 2017 1 commit
  3. 22 Nov, 2017 2 commits
  4. 21 Nov, 2017 1 commit
    • Robbert Krebbers's avatar
      Pattern matching notation for monadic binds. · dcd59f13
      Robbert Krebbers authored
      This gets rid of the old hack to have specific notations for pairs
      up to a fixed arity, and moreover allows to do fancy things like:
      
      ```
      Record test := Test { t1 : nat; t2 : nat }.
      
      Definition foo (x : option test) : option nat :=
        ''(Test a1 a2) ← x;
        Some a1.
      ```
      dcd59f13
  5. 20 Nov, 2017 2 commits
  6. 18 Nov, 2017 2 commits
  7. 16 Nov, 2017 2 commits
  8. 12 Nov, 2017 4 commits
  9. 11 Nov, 2017 2 commits
  10. 09 Nov, 2017 6 commits
  11. 03 Nov, 2017 1 commit
  12. 01 Nov, 2017 10 commits
  13. 31 Oct, 2017 2 commits