summaryrefslogtreecommitdiff
path: root/lib
Commit message (Expand)AuthorAge
...
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...Gravatar xleroy2008-05-30
* Suppression de 'exten', inutiliseGravatar xleroy2008-05-30
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Function -> Definition (probleme de performance avec Coq8.1pl3)Gravatar xleroy2008-01-07
* Ajout corollaires et overlap pour le papier JAR (pas encore utilises dans Com...Gravatar xleroy2007-12-08
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Utilisation de FunctionGravatar xleroy2007-03-23
* CommentairesGravatar xleroy2007-03-05
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...Gravatar xleroy2007-03-02
* Preuve des 2 axiomes restantsGravatar xleroy2007-03-02
* Ajout lemmes utiles sur egalite decidableGravatar xleroy2007-03-02
* Ajout operation eq dans PMap et IndexedMapGravatar xleroy2007-01-03
* Petites adaptations pour Coq 8.1gammaGravatar xleroy2006-11-11
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...Gravatar xleroy2006-10-22
* Fusion de la branche "traces":Gravatar xleroy2006-09-04
* Initial import of compcertGravatar xleroy2006-02-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 01:08:22 +0000