coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Allowing the abstract tactical to clear the environment from unused variables.	Pierre-Marie Pédrot	2015-08-22
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin	2015-08-02
\| *	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin	2015-08-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Fix for bug #4280: "decide equality produces terms that don't compute well".	Pierre-Marie Pédrot	2015-07-28
\| *	Fixing bug #3509 and #3510 (anomalies in "tactics/term_dnet.ml").	Pierre-Marie Pédrot	2015-07-28
* \|	Add an Iterative Deepening search strategy to typeclass resolution.	Matthieu Sozeau	2015-07-27
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	class_tactics: make interruptible	Enrico Tassi	2015-06-29
\| *	class_tactics: remove catch-all, use Errors.noncritical	Enrico Tassi	2015-06-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Fixing incompatibility introduced with simpl in commit 364decf59c1 (or	Hugo Herbelin	2015-06-23
\| *	With the field record punning syntax.	Theo Zimmermann	2015-06-23
\| *	Put all arguments of strategy in record.	Theo Zimmermann	2015-06-23
\| *	Strategy is now a record type with a function field.	Theo Zimmermann	2015-06-23
\| *	Add comments.	Theo Zimmermann	2015-06-23
* \|	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