• Robbert Krebbers's avatar
    Preparation to port the master branch · d60affc0
    Robbert Krebbers authored
    Major changes:
    * A data structure to collect locked addresses in memory.
    * Operations to lock and unlock addresses.
    * Remove [ctree_Forall] and express it using [Forall] and [ctree_flatten]. This
      saves a lot of lines of code.
    * Add a [void] value. This value cannot be typed, but will be used as a dummy
      return value for functions with return type [void].
    
    Minor changes:
    * Various deciders in preparation of the executable semantics.
    * Improve naming and notations.
    * Remove obsolete stuff.
    d60affc0
Name
Last commit
Last update
..
ars.v Loading commit data...
assoc.v Loading commit data...
base.v Loading commit data...
collections.v Loading commit data...
countable.v Loading commit data...
decidable.v Loading commit data...
fin_collections.v Loading commit data...
fin_map_dom.v Loading commit data...
fin_maps.v Loading commit data...
finite.v Loading commit data...
fresh_numbers.v Loading commit data...
lexico.v Loading commit data...
list.v Loading commit data...
listset.v Loading commit data...
listset_nodup.v Loading commit data...
map.v Loading commit data...
mapset.v Loading commit data...
natmap.v Loading commit data...
nmap.v Loading commit data...
numbers.v Loading commit data...
option.v Loading commit data...
orders.v Loading commit data...
pmap.v Loading commit data...
prelude.v Loading commit data...
proof_irrel.v Loading commit data...
tactics.v Loading commit data...
vector.v Loading commit data...
zmap.v Loading commit data...