coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-26	[attributes] [typing] Rename `typing` to `bypass_check`	Emilio Jesus Gallego Arias
	As discussed in the Coq meeting.
2020-11-26	[attributes] [doc] Documentation review by Théo.	Emilio Jesus Gallego Arias
	Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26	[proofs] Support per-definition typing-flags in interactive proofs.	Emilio Jesus Gallego Arias
	Most cases should be accounted in proof code, however be wary of paths where `Global.env ()` is used.
2020-11-26	[vernac] Allow to control typing flags with attributes.	Emilio Jesus Gallego Arias
	The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2019-08-16	Fix Print Assumptions: Inductive types can have unsafe fixpoints or	SimonBoulier
	type-in-type universes
2019-08-16	Universe Checking instead of Universes Checking	SimonBoulier

2019-08-16	Add a file for typing_flags in the test-suite.	SimonBoulier