coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR#449: make specialize smarter (bug 5370).	Maxime Dénès	2017-06-01
\|\
\| *	Tests for new specialize feature + CHANGES.	Pierre Courtieu	2017-05-31
\| \|
* \|	Documentation for eassert, eenough, epose proof, eset, eremember, epose.	Hugo Herbelin	2017-05-30
\|/ \| \| \|	Includes fixes and suggestions from Théo.
*	Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings	Maxime Dénès	2017-05-25
\|\
* \	Merge PR#406: coq makefile2	Maxime Dénès	2017-05-25
\|\ \
\| * \|	enters coq_makefile2	Enrico Tassi	2017-05-23
\| \| \|
* \| \|	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
\| *	Clarifying the interpretation path for the "constr_with_binding" argument.	Hugo Herbelin	2017-05-22
\|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility.
*	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès	2017-05-17
\|\
* \|	Aligning on standard layout of CHANGES.	Hugo Herbelin	2017-05-13
\| \|
\| *	Documenting Printing Compact Contexts + CHANGES	Pierre Courtieu	2017-05-11
\| \|
* \|	Tentative note in CHANGES about now applying βι while typing "match" branches.	Hugo Herbelin	2017-04-27
\|/ \| \| \| \| \| \|	In practice, this is almost invisible except when using "refine". So, in some sense, it is aligning the behavior of pretyping on the one of logic.ml's "refine" so that the more natural behavior of 8.4's refine on this issue is restored.
*	CHANGES entry for #545.	Maxime Dénès	2017-04-19
\|
*	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\
\| *	Documenting the changes introduced by the EConstr branch.	Pierre-Marie Pédrot	2017-04-10
\| \|
* \|	[camlpX] Enrico's changes to camlp4 removal.	Emilio Jesus Gallego Arias	2017-04-07
\|/ \| \| \| \|	This removes some remaining support for camlp4 in the infrastructure and documents the change.
*	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\
* \|	Document the changes to IZR.	Guillaume Melquiond	2017-03-22
\| \|
\| *	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \| \| \| \| \| \| \| \| \|	This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* \|	CHANGES: choice over setoids and prop. ext.	Hugo Herbelin	2017-03-03
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\|\
\| *	A few words in CHANGES.	Maxime Dénès	2016-12-07
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\|
\| *	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
\| \| \| \| \| \| \| \| \| \|	Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	[doc] Mention XML protocol on changes.	Emilio Jesus Gallego Arias	2016-11-16
\| \| \| \| \| \| \| \|	It may be worth it, also added a note about file reorganization.
\| *	Remove the list of bug fixes from CHANGES.	Maxime Dénès	2016-11-14
\| \| \| \| \| \| \| \| \| \|	We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear.
\| *	Update CHANGES and credits for 8.6beta1.	Maxime Dénès	2016-11-10
\| \|
\| *	Mention notypeclasses refine in CHANGES	Matthieu Sozeau	2016-11-07
\| \|
\| *	CHANGES for this branch.	Matthieu Sozeau	2016-11-07
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \|\
\| \| *	Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."	Maxime Dénès	2016-10-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses.
\| \| *	Update CHANGES.	Maxime Dénès	2016-10-25
\| \| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \|
* \| \|	Allocating a section in CHANGES for changes specific to 8.7.	Hugo Herbelin	2016-10-12
\| \| \|
\| * \|	Tentatively preparing to add changes specific to v8.7 (see PR #275).	Hugo Herbelin	2016-10-12
\|/ /
* \|	Report about changes of semantics of auto as an ltac argument (see #4966).	Hugo Herbelin	2016-10-08
\| \|
* \|	Remove the Set Verbose Compat option and turn the warning on by default.	Maxime Dénès	2016-10-06
\| \| \| \| \| \| \| \| \| \|	These warnings can now be configured like any other, so we don't need a specific option anymore.
* \|	Document change related to Keep Proof Equalities in CHANGES.	Maxime Dénès	2016-10-03
\| \|
* \|	Being more informative about the change of behavior of "subst".	Hugo Herbelin	2016-09-29
\| \|
* \|	Fix description of change in intro semantics.	Maxime Dénès	2016-09-21
\| \|
* \|	Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵	Hugo Herbelin	2016-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5.
* \|	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
\| \|
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\\|
\| *	Fixing CHANGES.	Hugo Herbelin	2016-08-17
\| \| \| \| \| \| \| \| \| \|	Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section.
* \|	Documenting fix of #3070 (subst and chain of dependencies).	Hugo Herbelin	2016-08-17
\| \|
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\\|
\| *	Fix #5000: Document the native compiler soundness bug due to Unicode mangling.	Pierre-Marie Pédrot	2016-08-07
\| \|
\| *	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \|	Modulo delta for types should be fully transparent.