coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-10	Merge PR #13821: Properly handle ordering of -w and -native-compiler	coqbot-app[bot]
	Reviewed-by: gares
2021-02-04	Remove deprecated -inputstate command line argument	Gaëtan Gilbert
	Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
2021-02-04	Properly handle ordering of -w and -native-compiler	Gaëtan Gilbert
	Warnings are handled as injection commands, interleaved with options and requires. Native compiler impacts require, so we must convert "yes" to "no" before handling injections. As such the semantic handling of the native command line argument must be separated from the emission of the warning message, which this PR implements. Fix #13819 In principle the other 2 cwarning in coqargs (deprecated spropcumul and inputstate) should be moved to injections too, but since they're deprecated I can't be bothered.
2021-01-27	make the linter happy	Enrico Tassi

2021-01-27	[coqargs] use standard option injection for -type-in-type	Enrico Tassi

2021-01-27	[coqc] move -output-context from sysinit/coqargs to coqc proper	Enrico Tassi

2021-01-27	[sysinit] move initialization code from coqtop to here	Enrico Tassi
	We also spill (some) non-generic arguments and initialization code out of coqargs and to coqtop, namely colors for the terminal. There are more of these, left to later commits.
2021-01-27	[sysinit] new component for system initialization	Enrico Tassi
	This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml