coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
	The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
2017-06-07	Put "ssreflect" behind "API".	Matej Košík

2017-06-06	Merge the ssr plugin.	Maxime Dénès