• 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
list.v 140 KB