coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-04-21	[flags] Deprecate is_silent/is_verbose in favor of single flag.	Emilio Jesus Gallego Arias
	Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
2017-04-15	Merge branch 'v8.6' into trunk	Maxime Dénès

2017-04-12	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵	Maxime Dénès
	record fields.
2017-04-07	Merge branch 'master' into econstr	Pierre-Marie Pédrot

2017-04-06	Merge PR#508: Optimize pending evars	Maxime Dénès

2017-04-04	Merge branch 'trunk' into pr379	Maxime Dénès

2017-04-01	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot
	For now we only normalize sorts, and we leave instances for the next commit.
2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès

2017-03-24	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin
	This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
2017-03-24	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin
	RawLocal -> CLocal
2017-03-24	Renaming local_binder into local_binder_expr.	Hugo Herbelin
	This is a bit long, but it is to keep a symmetry with constr_expr.
2017-03-24	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin

2017-03-23	Improving the API of constrexpr_ops.mli.	Hugo Herbelin
	Deprecating abstract_constr_expr in favor of mkCLambdaN, prod_constr_expr in favor of mkCProdN. Note: They did not do exactly the same, the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type, what I think is the correct thing to do. So, there is also a "fix" of semantic here.
2017-03-23	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot
	All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component.
2017-03-14	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias
	It was always set to `greedy:true`.
2017-02-15	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.