aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-0/+1
* Revised signed/unsigned char handling.xleroy2011-03-101-1/+0
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-1/+0
* Treat "char" as unsigned OR signed depending on the configuration.xleroy2011-03-091-0/+1
* Various algorithmic improvements that reduce compile times (thanks Alexandre ...xleroy2010-10-271-1/+1
* Updates for IA32-Cygwin.xleroy2010-09-081-3/+11
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-041-1/+2
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-0/+3
* Merge of branches/full-expr-4:xleroy2010-08-181-2/+4
* Support for inlined built-ins.xleroy2010-06-291-2/+2
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-1/+1
* Cleaner generation of .dependxleroy2010-03-301-2/+2
* New HTML documentation generatorxleroy2010-03-091-15/+11
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-2/+2
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-0/+1
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-9/+1
* Coloringaux: make identifiers unique; special treatment of precolored xleroy2009-08-261-1/+5
* Build bytecode version with debug symbols.xleroy2009-08-201-2/+2
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-171-1/+1
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-1/+1
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-1/+1
* Added 'going wrong' behaviorsxleroy2009-08-051-1/+1
* Various clean-upsv1.4xleroy2009-04-171-10/+27
* Added tail call optimization passxleroy2009-03-261-0/+1
* make install: ./ccomp au lieu de ../ccompblazy2009-02-271-1/+2
* Updatesxleroy2009-01-051-2/+9
* Wrong dependenciesxleroy2009-01-021-4/+6
* Continuation of ARM port.xleroy2009-01-011-7/+16
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-19/+40
* Revu removeproofxleroy2008-03-191-1/+8
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Ajout de common/Complements.vxleroy2007-08-261-1/+1
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-061-8/+15
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-16/+24
* Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de...xleroy2007-03-021-1/+1
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-1/+1
* Integration du front-end CIL developpe par Thomas Moniotxleroy2006-09-071-0/+8
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-7/+10
* Fusion de la branche "traces":xleroy2006-09-041-7/+11
* Initial import of compcertxleroy2006-02-091-0/+75
generated by cgit (git 2.34.1) at 2024-06-12 15:24:21 +0000