coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\
\| *	Fix bug #4159	Matthieu Sozeau	2015-05-27
\| *	Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".	Pierre-Marie Pédrot	2015-05-16
\| *	Granting wish #4048: Locate Ltac prints the source of redefined Ltac.	Pierre-Marie Pédrot	2015-05-15
* \|	Turning "Set Regular Subst Tactic" on by default (for 8.6).	Hugo Herbelin	2015-05-15
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Fixing bug #4216:	Pierre-Marie Pédrot	2015-05-13
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Adding an option Loose Hint Behavior to handle hints loaded but not imported.	Pierre-Marie Pédrot	2015-05-12
\| *	Adding unique identifiers to hints.	Pierre-Marie Pédrot	2015-05-12
\| *	Adding a test to check whether two tactic notations conflict.	Pierre-Marie Pédrot	2015-05-11
\| *	Fixing bug #4232.	Pierre-Marie Pédrot	2015-05-11
\| *	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
\| *	Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for	Hugo Herbelin	2015-05-09
\| *	Fixing treatment of recursive equations damaged by 857e82b2ca0d1.	Hugo Herbelin	2015-05-06
\| *	Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order	Hugo Herbelin	2015-05-06
\| *	Removing dead code in Rewrite.	Pierre-Marie Pédrot	2015-05-05
\| *	Making the strategy type in Rewrite opaque.	Pierre-Marie Pédrot	2015-05-05
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Code simplification in Tactics.	Pierre-Marie Pédrot	2015-05-04
\| *	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
\| *	Cleaning some uses of exceptions in tactics.	Pierre-Marie Pédrot	2015-04-25
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
\| *	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
\| *	Ensuring purity of datastructures in the API.	Pierre-Marie Pédrot	2015-04-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Cleaning up the implementation of search entries in Hints.	Pierre-Marie Pédrot	2015-04-14
\| *	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
\| *	Remove declarations of matched variables in change as an extension of	Matthieu Sozeau	2015-04-13
\| *	More documented representation of hint objects.	Pierre-Marie Pédrot	2015-04-13
\| *	Making the hint entry type opaque.	Pierre-Marie Pédrot	2015-04-12
\| *	Fix compilation broken by Matthieu's last commit.	Pierre Letouzey	2015-04-10
\| *	Fix #3590 for good this time, by changing the API, change's argument now	Matthieu Sozeau	2015-04-10
\| *	Eauto hints respect their priority. Fixes bug #3199.	Pierre-Marie Pédrot	2015-04-10
\| *	Making the hints for the auto tactics private.	Pierre-Marie Pédrot	2015-04-10
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Fix caching of local hintdb in typeclasses eauto.	Matthieu Sozeau	2015-04-09
\| *	refresh metas in rewrite hints loaded from .vo files (fix bug #3815)	Nickolai Zeldovich	2015-04-06
\| *	Removing a probably incorrect on-the-fly require in a tactic.	Pierre-Marie Pédrot	2015-04-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Aliasing give_up with admit	Enrico Tassi	2015-03-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| *	Reverting r10021 which enforces early assumptions on freshness which	Hugo Herbelin	2015-03-07
\| *	Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".	Hugo Herbelin	2015-03-07
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Fix bug #3590, keeping evars that are not turned into named metas by	Matthieu Sozeau	2015-03-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-28
\|\\|
\| *	Removing the unused field ltacrecvars of tactic internalization.	Pierre-Marie Pédrot	2015-02-27