coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	All arguments defined through ARGUMENT EXTEND declare a tactic scope.	Pierre-Marie Pédrot	2016-03-04
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
*	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
*	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\
\| *	Reporting about the new tactical unshelve.	Hugo Herbelin	2016-01-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	Update version numbers and magic numbers for 8.5rc1 release.	Maxime Dénès	2015-12-16
\| *	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond	2015-12-16
\| *	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	Updating CHANGES with an incompatibility.	Hugo Herbelin	2015-12-14
\| *	Flag -compat 8.4 now loads Coq.Compat.Coq84.	Maxime Dénès	2015-12-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Document removal of Set Virtual Machine and -vm in CHANGES.	Maxime Dénès	2015-12-11
\| *	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin	2015-12-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)	Hugo Herbelin	2015-12-05
\| *	Fix CHANGES.	Hugo Herbelin	2015-12-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-15
\|\\|
\| *	Update CHANGES	Jason Gross	2015-11-12
\| *	Fix bug #3735: interpretation of "->" in Program follows the standard one.	Matthieu Sozeau	2015-11-11
* \|	Listing separately changes from 8.5betas to final 8.5 and further	Hugo Herbelin	2015-11-10
* \|	Activating bracketing of last or-and introduction pattern by default	Hugo Herbelin	2015-11-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Update version numbers and magic numbers for 8.5beta3 release.	Maxime Dénès	2015-11-05
\| *	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau	2015-11-04
\| *	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	Mention bug 3199 fix as a source of incompatibilities.	Matthieu Sozeau	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Documenting the option "Strict Universe Declaration" in CHANGES.	Pierre-Marie Pédrot	2015-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Remove the "exists" overrides from Program. (Fix bug #4360)	Guillaume Melquiond	2015-10-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
\| *	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond	2015-09-28
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\|
\| *	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot	2015-09-25
\| *	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot	2015-09-25
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Explain new flags for native_compute in CHANGES.	Maxime Dénès	2015-09-16
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\\|
\| *	New option "Unset Bracketing Last Introduction Pattern" for preserving	Hugo Herbelin	2015-09-08
* \|	Documenting the new behaviour of the Shrink Obligations flag.	Pierre-Marie Pédrot	2015-09-08