aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)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
* -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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-04-23139-589/+9973
|\
| * 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-07 01:30:03 +0000