1. 27 Nov, 2016 6 commits
  2. 26 Nov, 2016 2 commits
  3. 25 Nov, 2016 11 commits
  4. 24 Nov, 2016 12 commits
  5. 23 Nov, 2016 9 commits
    • Ralf Jung's avatar
      opam: rename to coq-iris · d0743f7e
      Ralf Jung authored
      d0743f7e
    • Ralf Jung's avatar
      opam: build in parallel · 55ee8e66
      Ralf Jung authored
      55ee8e66
    • Ralf Jung's avatar
      start experimenting with opam · 4027fedc
      Ralf Jung authored
      4027fedc
    • Robbert Krebbers's avatar
      Fix typo. · 36c5a842
      Robbert Krebbers authored
      36c5a842
    • Ralf Jung's avatar
      Merge branch 'nclose_subseteq' into 'master' · f24fd7c3
      Ralf Jung authored
      Use notation N @⊆ E to avoid ambiguity.
      
      Since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be ill-typed.
      
      See merge request !24
      f24fd7c3
    • Ralf Jung's avatar
      Merge branch 'jh/fractional' into 'master' · 608e347c
      Ralf Jung authored
      Fractional typeclass.
      
      A typeclass for fractional assertions, that is assertions that depend on a fraction and that can be split.
      
      This is used to derive generically a few other instances for framing , destructing, combining and spliting assertions of sums of fractions. I found it usefull when doing fraction-heavy proofs in LambdaRust.
      
      The Right Way  To Do It would be to use a typeclass over the *predicate* itself. Unfortunately, the unification algorithm of typeclasses is not powerful enough to do the right beta-expansion that would expose the predicate applied to some fraction. Instead, the `Fractional` type class has as parameters both the predicate and the applied form that can be directly unified with the fractured assertion. Not very pretty.
      
      I wonder whether I should split this into two type classes: the first one would depend only on the predicate and would actually state the fractionality of it, and the second would do the beta-expansion job. What do you think?
      
      See merge request !23
      608e347c
    • Jacques-Henri Jourdan's avatar
      Fractional typeclass. · 50520536
      Jacques-Henri Jourdan authored
      50520536
    • Robbert Krebbers's avatar
      Eval hnf in iProof like in iPoseProof. · 0135f46c
      Robbert Krebbers authored
      0135f46c
    • Robbert Krebbers's avatar