Commits · c7995ce712dfc3c79f96f8c9cc16147b40ca1733 · Yixuan Chen / Iris

Feb 16, 2016
- we also need to go below mkSet for \notin · c7995ce7
  Ralf Jung authored 9 years ago
  
  c7995ce7
- provide a way to get bbelow mkSet · 60e1e123
  Ralf Jung authored 9 years ago
  
  60e1e123
Feb 15, 2016
- show that monadic set operations respect the partial order · ba30e046
  Ralf Jung authored 9 years ago
  
  ba30e046
Feb 13, 2016
- Use new Import/Export syntax everywhere. · bd7ebdec
  Robbert Krebbers authored 9 years ago
  
  Also, make our redefinition of done more robust under different orders of Importing modules.
  bd7ebdec
Nov 16, 2015
- Use qualified module names and coqc -Q instead of -R. · 8dc73363
  Robbert Krebbers authored 9 years ago
  
  8dc73363
Nov 11, 2015
- Initial commit · a123e160
  Robbert Krebbers authored 9 years ago
  
  a123e160