• Robbert Krebbers's avatar
    Partially revert "Explicit namespaces for counter, lock and spawn." · e67a4876
    Robbert Krebbers authored
    In order to improve flexibility, I have reverted the changes in commit
    5cabd278 to counter, lock and spawn because an explicit namespace may be in
    the way of modularity, for example, if the interfaces of these libraries will
    expose namespaces through view shifts in the future.
    
    Exposure of namespaces in the case of par is very unlikely, so to that end,
    par remains to use an explicit namespace.
    e67a4876
Name
Last commit
Last update
..
lib Loading commit data...
derived.v Loading commit data...
heap.v Loading commit data...
lang.v Loading commit data...
lifting.v Loading commit data...
notation.v Loading commit data...
proofmode.v Loading commit data...
tactics.v Loading commit data...
wp_tactics.v Loading commit data...