aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* add coq2html for pagesSylvain Boulmé2020-05-272-0/+7
|
* gitlab-ci.yml: inherit keyword does not work ?Sylvain Boulmé2020-05-271-2/+12
|
* pages: make documentationSylvain Boulmé2020-05-271-1/+5
|
* fix pages ?Sylvain Boulmé2020-05-271-0/+1
|
* basic pages configurationSylvain Boulmé2020-05-271-0/+9
|
* Merge remote-tracking branch 'certicompil/master' into kvx-workSylvain Boulmé2020-05-272-0/+26
|\
| * readmeDavid Monniaux2020-05-272-2/+17
| |
| * opam updateDavid Monniaux2020-05-271-0/+11
| |
* | link to the HAL preprintSylvain Boulmé2020-05-271-2/+6
| |
* | replace k1 -> kvxSylvain Boulmé2020-05-272-3/+3
|/
* install extra packagesDavid Monniaux2020-05-271-2/+2
|
* download/untar from KalrayDavid Monniaux2020-05-272-2/+3
|
* strict key checking offDavid Monniaux2020-05-271-1/+1
|
* CI for KVXDavid Monniaux2020-05-272-2/+17
|
* tests for kvxDavid Monniaux2020-05-26160-0/+0
|
* k1c -> kvx changesDavid Monniaux2020-05-26203-1057/+1057
|
* backport to coq 8.10.2Sylvain Boulmé2020-05-112-4/+9
|
* fix index-mppa_k1c.htmlSylvain Boulmé2020-05-111-1/+1
|
* updating the html index for mppa-k1cSylvain Boulmé2020-05-101-45/+27
| | | | NOTE: This file has been copied from the one of pldi-artefact branch.
* -fcse3-glbDavid Monniaux2020-05-066-14/+36
|
* CSE3 across mergesDavid Monniaux2020-05-065-11/+33
|
* make Aarch64 muladd depend on the optionDavid Monniaux2020-05-062-4/+10
|
* README KalrayCyril SIX2020-05-041-0/+32
|
* Adding copyrightsCyril SIX2020-05-04108-460/+1392
|
* Update on testsuite and INSTALL.mdCyril SIX2020-05-043-9/+16
|
* add a renumber phaseDavid Monniaux2020-04-301-0/+1
|
* run a separate CSE3 for LICMDavid Monniaux2020-04-241-1/+3
|
* Merge branch 'mppa-work' of ↵David Monniaux2020-04-23139-589/+9973
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Merge remote-tracking branch 'origin/mppa-features' into mppa-workDavid Monniaux2020-04-23139-589/+9973
| |\
| | * sync with licmDavid Monniaux2020-04-231-1/+1
| | |
| | * Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-237-35/+119
| | |\
| | | * CSE3 across callsDavid Monniaux2020-04-236-13/+44
| | | |
| | | * Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licmDavid Monniaux2020-04-235-21/+75
| | | |\
| | | | * make tracing output optionalDavid Monniaux2020-04-233-6/+11
| | | | |
| | | | * fix in CSE3 move propagationDavid Monniaux2020-04-234-42/+82
| | | | |
| | | | * CSE3analysisaux: pp_rhsDavid Monniaux2020-04-231-0/+9
| | | | |
| | | * | use cbn not simplDavid Monniaux2020-04-221-21/+21
| | | | |
| | * | | cbn and copyrightDavid Monniaux2020-04-222-9/+19
| | | | |
| | * | | use cbn in T instead of simpl in TDavid Monniaux2020-04-222-2/+3
| | | | |
| | * | | automated writing Compiler.vDavid Monniaux2020-04-226-122/+90
| | | | |
| | * | | generate mkpassDavid Monniaux2020-04-212-19/+14
| | | | |
| | * | | Require autogenDavid Monniaux2020-04-212-42/+26
| | | | |
| | * | | begin scripting the Compiler.v fileDavid Monniaux2020-04-215-39/+71
| | | | |
| | * | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-2115-165/+444
| | |\| |
| | | * | exampleDavid Monniaux2020-04-211-0/+6
| | | | |
| | | * | Merge branch 'mppa-cse3' of ../mppa-cse3 into mppa-licmDavid Monniaux2020-04-212-6/+34
| | | |\|
| | | | * improvement in precisionDavid Monniaux2020-04-212-6/+34
| | | | |
| | | * | Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licmDavid Monniaux2020-04-216-12/+18
| | | |\|
| | | | * forward moves through CSE3 storeDavid Monniaux2020-04-214-8/+11
| | | | |
| | | | * Merge remote-tracking branch 'origin/mppa-cse2' into mppa-cse3David Monniaux2020-04-2011-152/+393
| | | | |\
generated by cgit (git 2.34.1) at 2024-07-13 10:20:23 +0000