aboutsummaryrefslogtreecommitdiffstats
path: root/flocq
Commit message (Expand)AuthorAgeFilesLines
* Vendored Flocq library: address Coq 8.14 warningXavier Leroy2021-10-031-1/+1
* Update the vendored Flocq library to version 3.4.2Xavier Leroy2021-09-254-38/+20
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-2829-638/+1840
* Add FMA (fused multiply-add)Xavier Leroy2019-07-171-0/+121
* Make scripts compatible with new behavior of field_simplify (#291)Vincent Laporte2019-05-062-3/+3
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-2735-7394/+9493
* flocq: minor cleaning (#257)Vincent Laporte2018-09-141-3/+2
* Upgrade Flocq to version 2.6.1 from upstream (#71)Xavier Leroy2018-04-257-171/+420
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-284-14/+14
* Don't depend on the judgmental behavior of Bool.eqb (#217)Jason Gross2018-01-171-1/+1
* Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-0814-145/+119
* Update Flocq to version 2.5.2Xavier Leroy2017-02-138-132/+91
* The contradiction tactic has become more powerful.Maxime Dénès2017-01-091-2/+1
* Intro patterns have changed semantics...Maxime Dénès2017-01-091-0/+1
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-1/+1
* Upgrade to Flocq 2.5.0.Guillaume Melquiond2015-09-2220-1078/+2444
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-0717-646/+5920
* Update commentxleroy2014-08-131-2/+1
* Merge of "newspilling" branch:xleroy2014-07-231-0/+51
* Merge of Flocq version 2.2.0.xleroy2013-08-0229-223/+1908
* Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)xleroy2012-11-031-4/+4
* Use Flocq for floatsxleroy2012-06-2828-0/+17154
generated by cgit (git 2.34.1) at 2024-04-27 13:08:45 +0000