aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Heaps.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-021-3/+3
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-1/+1
* Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-0/+1
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-38/+38
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-79/+82
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-271-0/+570