Skip to content
Snippets Groups Projects
  1. Sep 20, 2017
  2. Sep 19, 2017
    • Robbert Krebbers's avatar
      Remove workaround. · 4cfa2e8a
      Robbert Krebbers authored
      This bug is strange:
      
      - In order to type check the argument `I : gmap lft lft_names`, Coq needs an
        instance `Countable lft`. Since `finite.finite_countable` has been declared
        using `Hint Immediate` it will try that instance first (*), which means it
        has to find an instance `Finite lft`.
      - Apparently, at this moment the type of the argument `A` has not been inferred
        by the type checker yet. So, there is a hypothesis `A : ?T`.
      - In order to prove `Finite lft`, Coq unifies `?T` with `Finite lft` and uses
        the hypothesis `A`.
      - Subsequent type checking fails, because `gmap lft lft_names` is type checked
        using a wrong/arbitrary instance `Countable lft`.
      
      This is probably a Coq bug: type class search should not just unify with
      hypotheses whose type is just an evar.
      
      (*) `finite.finite_countable` has been declared using `Hint Immediate` to make
      sure it is only used at leafs, not to make sure that it is used first.
      4cfa2e8a
    • Ralf Jung's avatar
      update Iris; get rid of opam.pins · cc1b8ab0
      Ralf Jung authored
      cc1b8ab0
  3. Aug 24, 2017
  4. Aug 23, 2017
  5. Aug 22, 2017
  6. Aug 21, 2017
  7. Aug 19, 2017
  8. Aug 16, 2017
  9. Aug 10, 2017
  10. Aug 08, 2017
  11. Aug 04, 2017
  12. Aug 03, 2017
  13. Aug 02, 2017
  14. Aug 01, 2017
  15. Jul 31, 2017
  16. Jul 19, 2017
  17. Jul 16, 2017
  18. Jul 11, 2017
  19. Jul 07, 2017
  20. Jul 06, 2017
Loading