1. 13 Mar, 2020 24 commits
  2. 29 Jan, 2019 24 commits
  3. 24 May, 2018 24 commits
    • Ralf Jung's avatar
      Remove the `default` notation for options · e585be6d
      Ralf Jung authored
      The notation was parsing-only and all it did was reorder the arguments for
      from_option.  This creates just a needless divergence between what is written
      and what is printed.  Also, removing it frees the name for maybe introducing a
      function or notation `default` with a type like `T -> option T -> T`.
      e585be6d
  4. 12 Nov, 2017 24 commits
    • Robbert Krebbers's avatar
      Make `fmap` left associative. · 12e701ca
      Robbert Krebbers authored
      This follows the associativity in Haskell. So, something like
      
        f <$> g <$> h
      
      Is now parsed as:
      
        (f <$> g) <$> h
      
      Since the functor is a generalized form of function application, this also now
      also corresponds with the associativity of function application, which is also
      left associative.
      12e701ca
  5. 08 Sep, 2017 24 commits
  6. 15 Mar, 2017 24 commits
  7. 31 Jan, 2017 24 commits
  8. 20 Sep, 2016 24 commits
  9. 27 Jul, 2016 24 commits
  10. 19 Feb, 2016 24 commits
  11. 17 Feb, 2016 24 commits
  12. 13 Feb, 2016 24 commits
  13. 16 Nov, 2015 24 commits
  14. 01 Feb, 2017 24 commits
    • Robbert Krebbers's avatar
      Port to Coq 8.5 beta 2. · 02f213ce
      Robbert Krebbers authored
      The port makes the following notable changes:
      
      * The carrier types of separation algebras and integer environments are no
        longer in Set. Now they have a type at a fixed type level above Set. This
        both works better in 8.5 and makes the formalization more general.
        I have tried putting them at polymorphic type levels, but that increased the
        compilation time by an order of magnitude.
      * I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
        That bug has been fixed, so this custom tactic can be removed when the next
        beta of 8.5 is out.
      02f213ce
  15. 08 Feb, 2015 24 commits
  16. 30 Sep, 2014 24 commits
  17. 16 Jun, 2014 24 commits
    • Robbert Krebbers's avatar
      Changes in preparation of the C type system and C front-end language · 3503a91f
      Robbert Krebbers authored
      Major changes:
      * Make void a base type, and include a proper void base value. This is necessary
        because expressions (free, functions without return value) can yield a void.
        We now also allow void casts conforming to the C standard.
      * Various missing lemmas about typing, weakening, decidability, ...
      * The operations "free" and "alloc" now operate on l-values instead of r-values.
        This removes some duplication.
      * Improve notations of expressions and statements. Change the presence of the
        operators conforming to the C standard.
      
      Small changes:
      * Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
        This gives more uniform notations.
      * New tactic "typed_inversion" performs inversion on an inductive predicate
        of type "Typed" and folds the premises.
      * Remove a horrible hack in the definitions of the classes "FMap", "MBind",
        "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
        defined a tactic "csimpl" that folds the results after performing an
        ordinary "simpl".
      * Fast operation to remove duplicates from lists using hashsets.
      * Make various type constructors (mainly finite map implementations) universe
        polymorphic by packing them into an inductive. This way, the whole C syntax
        can live in type, avoiding the need for (slow) universe checks.
      3503a91f
  18. 05 Jun, 2014 24 commits
    • 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
  19. 02 May, 2014 24 commits