Skip to content

1.1.0
Compare
Choose a tag to compare
@clayrat clayrat released this 23 Sep 16:37
· 46 commits to master since this release
v1.1.0
0caaa08
  • Allow for Coq 8.16 and Mathcomp 1.15
  • Switch to FCSL-PCM 1.6
  • Add specialized frame lemmas gU/stepU/tryU for passing an empty heap to a subroutine/recursive call
  • Refactor gE/stepE/tryE frames lemmas to produce separate goals for value and exception cases - the latter is typically trivial, saving one case invocation
  • Add GCD, binary (search) tree & cyclic buffer examples
Assets 2
Loading