aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Check for reserved keywords.Bernhard Schommer2019-05-101-1/+8
* Fix various scoping issues (#163)Bernhard Schommer2019-05-101-51/+56
* Ensure flushing of the error formatter.Bernhard Schommer2019-05-101-0/+4
* Expand the responsefiles earlierBernhard Schommer2019-05-105-17/+17
* Check for alignment of command-line switches.Bernhard Schommer2019-05-102-6/+10
* More efficient test for powers of twoXavier Leroy2019-05-092-26/+105
* Make scripts compatible with new behavior of field_simplify (#291)Vincent Laporte2019-05-062-3/+3
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-263-2/+2
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-2613-884/+1031
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-2315-135/+52
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-2311-68/+45
* Problems with Dwarf ranges (#159)Xavier Leroy2019-04-239-56/+96
|\
| * Simplified offset printing.Bernhard Schommer2019-04-161-2/+3
| * Print only debug info for printed functions.Bernhard Schommer2019-04-166-14/+18
| * Reworked range entries.Bernhard Schommer2019-04-163-39/+71
| * Reset scope ids later.Bernhard Schommer2019-04-161-1/+1
| * Avoid generation of empty ranges.Bernhard Schommer2019-04-161-1/+4
| * Relax requirement for ranges for compilation unit.Bernhard Schommer2019-04-161-1/+1
|/
* Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
* Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
* Floats.v: remove leftover Print commandsXavier Leroy2019-04-041-5/+1
* Floats.v: avoid using module Zlogarithm in the proofsXavier Leroy2019-04-031-10/+19
* Correct typo in Clightnorm.ml (#285)Alix Trieu2019-03-271-1/+1
* Ignore more of Coq's cache filesXavier Leroy2019-03-271-1/+4
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-2746-7841/+9954
* Define macros with CompCert's version number (#284)Xavier Leroy2019-03-271-2/+24
* Harden configure against weird Menhir installationsXavier Leroy2019-03-251-2/+8
* RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
* Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-252-3/+3
* Improve overflow check for integer literals (#157)Michael Schmidt2019-03-201-2/+4
* Update version number for 3.5v3.5Xavier Leroy2019-02-281-1/+1
* Update HTML doc for release 3.5Xavier Leroy2019-02-271-1/+1
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-261-1/+1
* Maximum supported Menhir version (#275)Xavier Leroy2019-02-261-1/+1
* Update Changelog in preparation for release 3.5Xavier Leroy2019-02-251-0/+35
* Maximum supported Menhir version (#275)Jacques-Henri Jourdan2019-02-251-2/+3
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-253-6/+29
* Reject object-related and struct-related attributes on typedefsXavier Leroy2019-02-254-8/+19
* Add regression test for "aligned" attributeXavier Leroy2019-02-253-1/+120
* Distinguish object-related and name-related attributesXavier Leroy2019-02-254-13/+24
* Do not expand type names when floating attributes "up" a declarationXavier Leroy2019-02-253-2/+24
* Ignore and clean file .lia.cacheXavier Leroy2019-02-122-1/+4
* Make the checker happy (#272)Vincent Laporte2019-02-123-19/+17
* Add support for Coq 8.9.0Xavier Leroy2019-02-041-3/+3
* <stddef.h>: define NULL with type void *Xavier Leroy2019-02-041-1/+1
* Test for NULL in variable argument listsXavier Leroy2019-02-042-1/+53
* <stdbool.h>: add missing macro __bool_true_false_are_definedXavier Leroy2019-02-041-0/+1
* Fix some URLs in the first page of the Coq HTML documentation (#263)Andre2019-01-221-5/+5
generated by cgit (git 2.34.1) at 2024-06-26 18:49:53 +0000