aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Locations.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-10/+10
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-5/+5
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-2/+2
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-171-8/+26
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-271-0/+22
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-56/+56
* Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.Xavier Leroy2015-08-221-1/+1
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-0/+8
* Merge of "newspilling" branch:xleroy2014-07-231-19/+42
* Merge of branch linear-typing:xleroy2014-04-061-19/+5
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-5/+19
* Revised division of labor between RTLtyping and Lineartyping:xleroy2014-03-271-19/+5
* Merge of the float32 branch: xleroy2013-05-191-10/+39
* Refactoring: move definition of chunk_of_type to AST.v.xleroy2013-05-061-1/+1
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-178/+223
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-3/+6
* Remove some useless "Require".xleroy2012-12-301-1/+0
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...xleroy2011-08-161-20/+15
* Locations.v: add Loc.diff_dec.xleroy2011-08-141-0/+9
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+23
* Support for inlined built-ins.xleroy2010-06-291-0/+23
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-2/+2
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-89/+4
* Revised back-end so that only 2 integer registers are reserved for reloading.xleroy2008-12-211-8/+8
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-1/+1
* Initial import of compcertxleroy2006-02-091-0/+476