compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Adapt w.r.t. coq/coq#15442 (#425)	Pierre-Marie Pédrot	2022-01-10	1	-2/+2
\| \| \| \| \| \| \|	coq/coq#15442 changes the way `Program` names things, to make it uniform w.r.t. the standard naming schema. This commit removes dependencies on the names chosen by `Program`. Should be backwards compatible. Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr>
*	Use the LGPL instead of the GPL for dual-licensed files	Xavier Leroy	2021-05-08	1	-4/+5
\| \| \| \| \| \|	The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
*	Qualify `Hint` as `Global Hint` where appropriate	Xavier Leroy	2021-01-21	1	-1/+1
\| \| \| \| \| \| \|	This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
*	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-22/+22
\| \| \| \| \| \| \| \| \| \| \|	Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
*	Ensure FunInd or Recdef is imported if functional induction is used	Sigurd Schneider	2017-07-20	1	-1/+1
\| \| \| \| \| \|	Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
*	Port to Coq 8.5pl2	Xavier Leroy	2016-07-08	1	-5/+1
\| \| \| \| \|	Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-23/+23
\|
*	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	xleroy	2011-03-09	1	-4/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-0/+319
	- Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e