compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Improve portability of the test for annotations inclightgen	Xavier Leroy	2020-06-05	1	-0/+2
\| \| \| \|	__builtin_ais_annot is not supported for macOS nor for Cygwin.
*	clightgen: fix the printing of annotations	Xavier Leroy	2020-06-05	1	-0/+6
	The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360