aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
* Added error for redefined builtin.Bernhard Schommer2020-07-203-0/+6
* Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
* Bytecode-only build, continuedXavier Leroy2020-07-151-0/+9
* Revised detection of menhirLib directory, continued (#365)Xavier Leroy2020-07-151-4/+4
* No trailing commas for --version-file option.Bernhard Schommer2020-07-091-1/+1
* Fix typo.Bernhard Schommer2020-07-081-1/+1
* Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
* Use the same version string.Bernhard Schommer2020-07-081-10/+3
* Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
* Introduce additional "branch" build information.Bernhard Schommer2020-07-087-13/+20
* Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
* Bytecode-only build (#243)Xavier Leroy2020-07-072-4/+29
* Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
* Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
* Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
* Added missing hint database name.Bernhard Schommer2020-06-301-1/+1
* Move shared code in new file.Bernhard Schommer2020-06-2817-96/+46
* Remove the `can_reserve_register` function.Bernhard Schommer2020-06-2810-19/+1
* Use library function.Bernhard Schommer2020-06-281-4/+1
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-288-9/+8
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-252-40/+54
* Improve printing of builtin function invocationsXavier Leroy2020-06-251-0/+3
* Preliminary support for Coq 8.12Xavier Leroy2020-06-212-4/+4
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-213-3/+3
* SimplExpr: remove unused definition "sd_cast_set"Xavier Leroy2020-06-151-2/+0
* SimplExpr: better translation of casts in a "for effects" contextXavier Leroy2020-06-153-136/+166
* Compatibility with coq 8.11.2Bernhard Schommer2020-06-081-1/+1
* Improve portability of the test for annotations inclightgenXavier Leroy2020-06-052-0/+4
* clightgen: fix the printing of annotationsXavier Leroy2020-06-052-59/+14
* clightgen: fix usage messageXavier Leroy2020-06-011-2/+2
* clightgen -short-idents : do not use $"xxx" notation everXavier Leroy2020-06-011-1/+1
* Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-194-20/+204
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+0
* Update the list of dual-licensed filesXavier Leroy2020-05-051-2/+2
* Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
* Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
* Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
* Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
* Do not use "Declare Scope", introduced in Coq 8.10 onlyXavier Leroy2020-05-041-1/+0
* Coq-MenhirLib: explicit import ListNotations (#354)Jacques-Henri Jourdan2020-05-047-4/+12
* Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-292-1/+19
* Updated .gitignoreBernhard Schommer2020-04-271-0/+1
* Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
* Move reserved_registers to CPragmas.Bernhard Schommer2020-04-204-8/+8
* Support for coq 8.11.1.Bernhard Schommer2020-04-201-2/+2
* Check for errors after each pass.Bernhard Schommer2020-04-201-1/+8
* Added warning for packed composite with bitfields.Bernhard Schommer2020-04-201-0/+2
* Add location to transform functions.Bernhard Schommer2020-04-204-28/+28
* Updates for release 3.7v3.7Xavier Leroy2020-03-311-1/+1
* Updates for release 3.7Xavier Leroy2020-03-312-1/+6
generated by cgit (git 2.34.1) at 2024-06-30 23:09:13 +0000