aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Registers.v
Commit message (Expand)AuthorAgeFilesLines
* Give explicit scopes to notations a#b and a##b and a#b<-cXavier Leroy2017-02-131-3/+5
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-1/+1
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-0/+36
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-3/+3
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-3/+4
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-021-2/+4
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-1/+0
* Initial import of compcertxleroy2006-02-091-0/+49