aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Coqlib.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-2/+80
|\
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-151-2/+0
| * 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-081-4/+5
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-191-20/+0
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-24/+5
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-70/+74
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-10/+10
| * Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-58/+54
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-0/+35
* | centralize if_sameDavid Monniaux2020-10-091-0/+6
|/
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-89/+5
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-30/+7
* Import prim token notations before using themJason Gross2018-08-271-0/+1
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-50/+50
* Removed some implict arguments.Bernhard Schommer2016-09-051-5/+3
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-2/+3
* Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-061-0/+56
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-89/+89
* Merge of the "princeton" branch:xleroy2013-06-161-0/+3
* Coq-defined equality functions for Allocation.xleroy2013-05-011-0/+7
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+21
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-0/+48
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-1/+2
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-57/+29
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-4/+4
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-0/+14
* Merge of the newmem branch:xleroy2012-05-211-18/+1
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-0/+43
* Back from Oregon commit. xleroy2011-07-051-0/+14
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-1/+4
* Typo in documentationxleroy2010-05-261-1/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+127
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-5/+23
* Cleaned up list_drop.xleroy2009-11-181-34/+28
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-101-0/+7
* Added support for jump tables in back end.xleroy2009-11-101-0/+74
* Added 'going wrong' behaviorsxleroy2009-08-051-0/+5
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-60/+60
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-0/+25
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-0/+86
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+40
* Ajout lemmes utiles sur egalite decidablexleroy2007-03-021-0/+31
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-0/+1
* Lever la restriction sur les fonctions externes, restriction qui exigeait que...xleroy2006-10-221-1/+43
generated by cgit (git 2.34.1) at 2024-05-09 08:09:00 +0000