Skip to content
Snippets Groups Projects
Select Git revision
  • fix-export
  • instance-nobody-open-proof
  • ralf/notation
  • master default protected
  • robbert/set_rename
  • robbert/map_seq
  • ci/debug
  • ci/opam2
  • ci/perf
  • ci/buildcache
  • ci/ralf/mangled
  • ralf/exact_vm_cast
  • ci/coqdoc
  • ci/artifacts
  • coq-stdpp-1.0
  • options
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
18 results
Compare
Forked from Iris / stdpp
2469 commits behind the upstream repository.
user avatar
Make hlist universe polymorphic.
Robbert Krebbers authored 
This change makes it possible to use hlists in the proof mode, which
itself uses hlists in the implementation of the specialize tactic.
4420aa4d
History
user avatar 4420aa4d
History
Name Last commit Last update
theories