coq - The formal proof system

Age	Commit message (Collapse)	Author
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 -print-emacs	Enrico Tassi

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

2021-01-27	[coqargs] use standard option injection for -mangle-names	Enrico Tassi

2021-01-27	[coqtop] handle -print-module-uid after initialization	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