• 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
nmap.v 3.82 KB