aboutsummaryrefslogtreecommitdiffstats
path: root/lib/UnionFind.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-0/+1
|\
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-0/+1
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-4/+4
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-3/+3
* | Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
|/
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-49/+49
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-56/+56
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-64/+80
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-9/+5
* Unionfind data structure, used in new implementation of backend/Tunnelingxleroy2009-08-161-0/+702