aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* Update warning flags used to compile Flocq and MenhirlibXavier Leroy2023-03-101-2/+5
* When installing the Coq development, also install coq-native generated filesXavier Leroy2023-02-201-1/+6
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-191-4/+0
* Check early that extraction did not run into unimplemented axiomsXavier Leroy2022-07-071-0/+5
* Update comment about `deprecated-hint-rewrite-without-locality` warningXavier Leroy2022-07-071-4/+0
* Re-enable `deprecated-hint-rewrite-without-locality` warningXavier Leroy2022-07-051-2/+1
* Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-251-3/+2
* Selectively turn some Coq 8.14 warnings offXavier Leroy2021-10-031-1/+11
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-3/+11
* Refactor clightgenXavier Leroy2021-09-221-4/+4
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-281-0/+1
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-7/+23
* Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
* Bytecode-only build, continuedXavier Leroy2020-07-151-0/+9
* Introduce additional "branch" build information.Bernhard Schommer2020-07-081-1/+4
* Preliminary support for Coq 8.12Xavier Leroy2020-06-211-1/+1
* Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-291-1/+18
* Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
* Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-1/+1
* Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-1/+1
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+11
* Type inference and type checking for CminorXavier Leroy2019-06-061-1/+1
* Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-171-12/+12
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-1/+1
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+1
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+8
* Ignore and clean file .lia.cacheXavier Leroy2019-02-121-0/+1
* Make the checker happy (#272)Vincent Laporte2019-02-121-5/+1
* Make generated file cparser/Parser.v read-onlyXavier Leroy2018-08-271-0/+2
* Ensure compatibility with Menhir before and after version 20180530Xavier Leroy2018-06-061-1/+1
* Fix menhirLib namespaces, following changes in Menhir version 20180530Jacques-Henri Jourdan2018-06-061-2/+2
* Use the standalone coq2html tool to generate the HTML documentationXavier Leroy2018-06-011-10/+2
* Install the VERSION file along the .vo filesBenoît Viguier2018-05-311-0/+1
* Install Coq development (.vo files) if requested (#232)Xavier Leroy2018-05-301-1/+10
* Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-251-0/+3
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-281-3/+0
* Removed no longer needed struct passing.Bernhard Schommer2018-02-261-2/+0
* Fix check-proof target of the Makefile after merge of Coq #6277.Pierre-Marie Pédrot2017-12-071-1/+1
* Makefile: chmod a-w instead of chmod -wXavier Leroy2017-09-111-1/+1
* Update the "make check-proof" entry for Coq 8.6Xavier Leroy2017-03-241-3/+2
* Turn warning "deprecated-implicit-arguments" off while compiling FlocqXavier Leroy2017-02-131-1/+4
* Also remove coq aux files.Bernhard Schommer2017-01-241-0/+1
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-1/+1
* Merge pull request #145 from AbsInt/64Xavier Leroy2016-10-271-10/+26
|\
| * Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-8/+23
| * Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-2/+3
generated by cgit (git 2.34.1) at 2024-05-04 05:11:13 +0000