1. 06 Sep, 2021 1 commit
    • Armaël Guéneau's avatar
      Optimize iIntoEmpValid · 20b0a19d
      Armaël Guéneau authored
      With large proof contexts and lemmas with many forall quantifiers,
      iIntoEmpValid can become quite slow. This makes it go faster by adding
      "fast paths" for the -> and forall cases, gated by Ltac pattern
      matching (which is faster than trying to unify with refine and fail).
      20b0a19d
  2. 01 Sep, 2021 1 commit
  3. 30 Jul, 2021 2 commits
  4. 28 Jul, 2021 2 commits
  5. 26 Jul, 2021 5 commits
  6. 25 Jul, 2021 2 commits
  7. 23 Jul, 2021 2 commits
  8. 22 Jul, 2021 2 commits
  9. 19 Jul, 2021 1 commit
  10. 18 Jul, 2021 2 commits
  11. 16 Jul, 2021 1 commit
  12. 20 Jun, 2021 1 commit
  13. 19 Jun, 2021 1 commit
    • Paolo G. Giarrusso's avatar
      Mode for Equiv · 5f5c02af
      Paolo G. Giarrusso authored
      Include workaround for Coq bug #14441, and drop now-failing test for that Coq
      bug.
      5f5c02af
  14. 18 Jun, 2021 3 commits
  15. 17 Jun, 2021 2 commits
  16. 08 Jun, 2021 1 commit
  17. 07 Jun, 2021 1 commit
  18. 06 Jun, 2021 1 commit
  19. 02 Jun, 2021 1 commit
  20. 31 May, 2021 2 commits
  21. 27 May, 2021 1 commit
    • Jacques-Henri Jourdan's avatar
      Change the tactic for resolving typeclass instances from canonical structures. · 011e9bbb
      Jacques-Henri Jourdan authored
      Example include Equiv, Dist, Op, Core, Valid, ValidN and Unit.
      
      The previous hints used eapply. The new hint now use refine. These two
      tactic use a different unification algorithm, which result in
      different behavior with respect to canonical structures.
      
      The refine tactic is followed by shelving all the remaining goals,
      which correspond actually to existential variables.
      
      In particular, in RustHornBelt, the version using apply is unable to
      find the canonical structure of heterogeneous lists.
      011e9bbb
  22. 26 May, 2021 5 commits