1. 04 Feb, 2017 40 commits
  2. 03 Feb, 2017 40 commits
  3. 31 Jan, 2017 40 commits
  4. 09 Dec, 2016 40 commits
  5. 08 Dec, 2016 40 commits
  6. 06 Dec, 2016 40 commits
  7. 05 Dec, 2016 40 commits
    • Robbert Krebbers's avatar
      New definition of contractive. · 3caefaaa
      Robbert Krebbers authored
      Using this new definition we can express being contractive using a
      Proper. This has the following advantages:
      
      - It makes it easier to state that a function with multiple arguments
        is contractive (in all or some arguments).
      - A solve_contractive tactic can be implemented by extending the
        solve_proper tactic.
      3caefaaa
  8. 29 Nov, 2016 40 commits
  9. 24 Nov, 2016 40 commits
  10. 23 Nov, 2016 40 commits
    • Robbert Krebbers's avatar
      Fix typo. · ed15664a
      Robbert Krebbers authored
      ed15664a
    • Ralf Jung's avatar
      Merge branch 'nclose_subseteq' into 'master' · 492a6bc7
      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
      492a6bc7