aboutsummaryrefslogtreecommitdiffstats
path: root/common/Switch.v
Commit message (Expand)AuthorAgeFilesLines
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-101-4/+4
* Update comment re: compile_switch functionXavier Leroy2022-06-251-1/+1
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-19/+19
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-3/+3
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-5/+5
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-26/+26
* Excessively strict validation: ofs + sz < modulus should have beenxleroy2014-08-201-4/+5
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-171/+165
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-39/+58
* Updated PowerPC port to new integers.xleroy2013-02-121-1/+1
* Merge of branch "unsigned-offsets":xleroy2011-04-091-17/+16
* Added support for jump tables in back end.xleroy2009-11-101-12/+131
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-2/+2
* Amelioration compilation des switchxleroy2008-04-171-30/+70
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+165