aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Maps.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-011-583/+762
|\
| * Maps.v: transparency of NodeXavier Leroy2021-11-161-1/+3
| * An improved PTree data structure (#420)Xavier Leroy2021-11-161-478/+748
* | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-2/+2
|\|
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-2/+2
| * 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-65/+84
|\|
| * Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| * Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-93/+44
|\ \
| * | set_disjointDavid Monniaux2019-12-131-0/+49
| |/
* | progress on wellformed regDavid Monniaux2020-02-051-1/+120
* | gremove_tDavid Monniaux2020-02-041-0/+36
* | gcombine_nullDavid Monniaux2020-02-041-0/+13
* | gcombine_nullDavid Monniaux2020-02-041-1/+39
|/
* Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-051-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-9/+9
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-131-2/+2
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-51/+51
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...Xavier Leroy2016-05-071-0/+80
* Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-061-34/+133
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-113/+113
* remove not used hypotheses in TREEJacques-Henri Jourdan2015-03-251-9/+4
* Add theorem "elements_remove".Xavier Leroy2014-09-241-167/+178
* More efficient implementations of map, fold, etc.xleroy2014-08-271-164/+109
* Small improvements in compilation times for the register allocation pass.xleroy2013-09-201-0/+39
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-330/+194
* Bind some local defs with Let, makes extracted code cleanerv1.13xleroy2013-03-121-2/+2
* Maps: revised TREE interface; added mucho derived properties and operations i...xleroy2013-03-121-59/+248
* Useless Importxleroy2013-03-101-1/+0
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-34/+52
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-21/+5
* Memdata: cleanup continuedxleroy2012-05-261-0/+26
* Merge of the newmem branch:xleroy2012-05-211-4/+96
* Cleaned up old commented-out partsxleroy2011-08-191-5/+0
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-271-2/+22
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+77
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-42/+56
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-1/+35
* Added 'going wrong' behaviorsxleroy2009-08-051-0/+115
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-130/+130
* Suppression de 'exten', inutilisexleroy2008-05-301-6/+0
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-021-0/+82
* Ajout operation eq dans PMap et IndexedMapxleroy2007-01-031-0/+10
* Initial import of compcertxleroy2006-02-091-0/+1034
generated by cgit (git 2.34.1) at 2024-05-09 18:41:31 +0000