coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-10-04	Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).	Maxime Dénès

2017-09-28	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot

2017-09-28	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot
	The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
2017-09-26	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès

2017-09-25	Merge PR #1060: An optimization of tactic constructor	Maxime Dénès

2017-09-21	Mark "Set Tactic Compat Context" as deprecated.	Guillaume Melquiond
	It was introduced in 8.5 for compatibility with a 8.4 bug.
2017-09-19	An optimization of tactic constructor.	Hugo Herbelin
	As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time.
2017-09-19	Fixing bug #5741 (anomaly in info_trivial).	Hugo Herbelin
	The bug was introduced in 1559f73.
2017-09-19	Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).	Maxime Dénès

2017-09-19	Don't lose names in UState.universe_context.	Gaëtan Gilbert
	We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
2017-09-15	Merge PR #1046: Better error messages, fix for BZ#5723	Maxime Dénès

2017-09-15	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès

2017-09-15	Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵	Maxime Dénès
	Inductive-keyworded record failing even on non-dependent goal)
2017-09-14	Avoid extra failure in the "constructor" tactic (bug #5666).	Guillaume Melquiond
	This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n.
2017-09-11	Better error messages, fix for BZ#5723	Paul Steckler

2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
	When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
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-08-30	Fixing part of #5707 (allowing destruct to use non dependent case analysis).	Hugo Herbelin
	The fix covers the case of a non-dependent goal with unavailable dependent case analysis: destruct was not seeing that it could still use non-dependent case analysis.
2017-08-29	Fix BZ#5697: Congruence does not work with primitive projections.	Pierre-Marie Pédrot
	The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records.
2017-08-29	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès

2017-08-29	Merge PR #805: Functional tactics	Maxime Dénès

2017-08-01	Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).	Maxime Dénès

2017-08-01	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès

2017-07-31	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès

2017-07-31	better `try with` scope in `discr_positions`	amblaf

2017-07-31	Correcting [build_discriminator] to make the test-suite pass	amblaf

2017-07-31	Replacing tclENV with the goal environment	amblaf
	In functions match_eqdec and check_unused_names
2017-07-31	env, sigma as first arguments of functions	amblaf

2017-07-31	Remove references to Global.env in tactics/*.ml	amblaf
	Only in ml files that are not related to Coq commands
2017-07-28	Merge PR #888: Stronger kernel types	Maxime Dénès

2017-07-27	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin

2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-26	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot

2017-07-26	More precise type for universe entries.	Pierre-Marie Pédrot
	We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
2017-07-26	Merge PR #868: Fix debug trace of typeclasses eauto.	Maxime Dénès

2017-07-20	Merge PR #892: Improve do_split option of typeclass resolution	Maxime Dénès

2017-07-20	Merge PR #899: [general] Move files to directories so they match linking order.	Maxime Dénès

2017-07-20	Merge PR #869: Enforce alternating separators in typeclass debug output	Maxime Dénès

2017-07-20	Merge branch 'v8.7'	Maxime Dénès

2017-07-19	[general] Move files to directories matching linking order.	Emilio Jesus Gallego Arias
	We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.
2017-07-19	Fix debug trace of typeclasses eauto.	Théo Zimmermann

2017-07-18	Improve do_split option of typeclass resolution	Matthieu Sozeau
	It used to compute the dependencies of all undefined evars of the evar_map, while only the dependencies of resolvable evars are necessary.
2017-07-14	Getting rid of abstraction breaking code in tclABSTRACT.	Pierre-Marie Pédrot
	This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch.
2017-07-13	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot

2017-07-13	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot

2017-07-13	Getting rid of AUContext abstraction breakers in Elimschemes.	Pierre-Marie Pédrot

2017-07-12	format pairs of items for pr_depth to get alternating separators	Paul Steckler
	eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
2017-07-11	Backtracking on deprecation of Bracketing Last Intro Pattern.	Théo Zimmermann
	As per @JasonGross's request who described a use case for this option in https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative solution for this use case.
2017-07-11	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann

2017-07-11	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot
	Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.