aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-2130-133/+136
| | * Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | * "macosx" is now called "macos"Xavier Leroy2021-01-1816-25/+25
| | * macOS: turn #warning offXavier Leroy2021-01-181-2/+2
| | * Remove regression/interop1 testXavier Leroy2021-01-184-417/+1
| | * Testing calling conventions and interoperability with another C compilerXavier Leroy2021-01-185-1/+583
| | * Support re-normalization of function parameters at function entryXavier Leroy2021-01-167-27/+58
| | * Change warning for pragmas inside functionsXavier Leroy2021-01-161-1/+1
| | * PowerPC: wrong computation of the position of the first vararg argumentXavier Leroy2021-01-151-2/+3
| | * Coq 8.13.0 is supportedXavier Leroy2021-01-141-3/+3
| | * RISC-V: fix FP calling conventionsXavier Leroy2021-01-146-122/+176
| | * Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| | * Improve branch tunnelingXavier Leroy2021-01-132-60/+328
| | * Revised correctness proof for record_gotoXavier Leroy2021-01-131-68/+29
| | * Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | * Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| | * RISC-V: wrong fixup code generated for vararg calls with fixed FP argsXavier Leroy2021-01-103-12/+35
| | * Ignore and warn about pragmas inside functionsXavier Leroy2021-01-071-1/+4
| | * Replace `omega` tactic with `lia`Xavier Leroy2020-12-29110-2695/+2694
| | * Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
| | * Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-2830-638/+1841
| | * configure: simplify the final printing of the configurationXavier Leroy2020-12-281-9/+8
| | * configure: add -mandir option (#382)Daniel Dickman2020-12-281-1/+7
| | * AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)Xavier Leroy2020-12-261-1/+1
| | * AArch64: macOS portXavier Leroy2020-12-2618-220/+570
| | * C parser: handle other built-in types than __builtin_va_listXavier Leroy2020-12-261-1/+2
| | * AArch64: clarify the printing of extending-register arithmetic operationsXavier Leroy2020-12-261-13/+13
| | * AArch64: wrong function alignmentXavier Leroy2020-12-261-1/+1
| | * RISC-V: revised calling conventions for variadic functionsXavier Leroy2020-12-252-63/+105
| | * Changed cc_varargs to an option typeBernhard Schommer2020-12-2512-27/+36
| | * configure: use `$make` instead of `make`Xavier Leroy2020-12-251-1/+1
| | * configure script revised and simplifiedXavier Leroy2020-12-241-83/+43
| | * configure: support Coq 8.12.2Xavier Leroy2020-12-241-2/+2
| | * Configure the correct archiver to build runtime/libcompcert.aXavier Leroy2020-12-242-2/+8
| | * x86 32 bits: ABI non-conformance for functions returning structs/unionsXavier Leroy2020-12-111-1/+1
| | * Error when using -main without -interpXavier Leroy2020-12-061-0/+2
| | * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | * ARM modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | * AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
* | | No inline when no load and store are presentYann Herklotz2021-02-231-1/+7
|/ /
* | Fix dune file as wellYann Herklotz2020-11-271-1/+1
* | Add proof of splitlong_ptr32Yann Herklotz2020-11-271-0/+3
* | Add Verilog backendYann Herklotz2020-11-2733-0/+16929
* | Always try inlining functionsYann Herklotz2020-11-271-4/+1
* | Ignore unnecessary foldersYann Herklotz2020-11-272-1/+1
|/
* Updates for release 3.8v3.8Xavier Leroy2020-11-163-5/+10
* Do not use -warn-error when building from a release tarballXavier Leroy2020-11-141-2/+9
* Support Coq 8.12.1Xavier Leroy2020-11-142-3/+3
* Update READMEXavier Leroy2020-11-091-4/+4
generated by cgit (git 2.34.1) at 2024-05-17 11:14:03 +0000