aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-102-2/+7
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-221-1/+1
* Replace CR, FF and VT with whitespace.Bernhard Schommer2022-11-051-3/+5
* Use open_in_bin instead of open_in.Bernhard Schommer2022-11-051-1/+1
* Add `Commandline.longopt` function for options of the form `-<key>=<arg>`Xavier Leroy2022-09-232-20/+18
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-081-2/+2
* Add [#global] qualifier on Hint Rewrite (#439)Pierre-Marie Pédrot2022-07-051-0/+8
* Extend the boolean_equality tactic (#429)Jerome Hugues2022-06-251-1/+15
* Upgrade to Flocq 4.1.Guillaume Melquiond2022-04-261-2/+2
* Upgrade to Flocq 4.0.Guillaume Melquiond2022-04-252-148/+132
* Introduce float_conversion_default_nan parameter for float-float conversionsBernhard Schommer2022-04-251-2/+7
* Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-101-2/+2
* Maps.v: transparency of NodeXavier Leroy2021-11-161-1/+3
* An improved PTree data structure (#420)Xavier Leroy2021-11-162-638/+902
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-032-23/+23
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-154-2/+4
* Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+112
* Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
* Add `floor` and some propertiesXavier Leroy2021-07-261-0/+37
* More lemmas about `align`Xavier Leroy2021-07-261-0/+17
* More lemmas about list appendXavier Leroy2021-07-261-0/+26
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0831-124/+155
* Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-20/+0
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-213-33/+36
* Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
* Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
* Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2914-1026/+1022
* Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
* Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
* Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-191-3/+76
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
* 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
* Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
* Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-7/+9
* AArch64 portXavier Leroy2019-08-081-24/+136
* More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
* Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
* Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
* Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
* Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
* Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+2
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
generated by cgit (git 2.34.1) at 2024-05-03 23:22:21 +0000