aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-102-9/+9
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-222-3/+3
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-195-1/+8
* Introducing the "eventually" closure and new simulation diagrams using itXavier Leroy2022-09-051-27/+229
* Support mergeable sections for fixed-size literalsXavier Leroy2022-08-292-13/+19
* Add [#global] qualifier on Hint Rewrite (#439)Pierre-Marie Pédrot2022-07-051-0/+4
* Update comment re: compile_switch functionXavier Leroy2022-06-251-1/+1
* Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-102-4/+4
* An improved PTree data structure (#420)Xavier Leroy2021-11-162-19/+1
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-10/+10
* Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-1/+1
* For numerical builtins, support return types that are small integer typesXavier Leroy2021-09-221-25/+47
* Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-152-1/+2
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0822-88/+110
* Support __builtin_unreachableXavier Leroy2021-05-021-0/+5
* Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-192-15/+15
* Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
* Section handling: finer control of variable initializationXavier Leroy2021-02-232-25/+54
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-216-12/+12
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2912-382/+382
* Changed cc_varargs to an option typeBernhard Schommer2020-12-251-5/+5
* Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+1
* Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+5
* Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-211-1/+1
* Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-292-10/+23
* Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
* Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-14/+30
* Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-15/+33
* Refine the type of function results in AST.signatureXavier Leroy2020-02-219-80/+189
* Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-112-3/+23
|\
| * Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
| * Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
| * Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
| * Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-072-6/+6
* | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+23
* | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-052-6/+6
|/
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-8/+647
* Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-2/+2
* Support a "select" operation between two valuesXavier Leroy2019-05-201-0/+126
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-4/+5
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-234-11/+11
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-234-20/+20
* Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
* Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-271-41/+53
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-052-0/+6
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+34
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-1/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-1/+1
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-195-11/+13
generated by cgit (git 2.34.1) at 2024-05-04 05:29:18 +0000