coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\
\| *	Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.	Pierre-Marie Pédrot	2015-11-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau	2015-11-04
\| *	Fix bug #4151: discrepancy between exact and eexact/eassumption.	Matthieu Sozeau	2015-11-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Fixing another instance of bug #3267 in eauto, this time in the	Hugo Herbelin	2015-10-29
* \|	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Generalize fix for auto from PMP to eauto and typeclasses eauto.	Matthieu Sozeau	2015-10-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Refine fix for handling of the universe contexts of hints, depending on	Matthieu Sozeau	2015-10-09
\| *	Fix CFGV contrib: handling of global hints introducing global universes.	Matthieu Sozeau	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
\| *	Fix compilation broken by Matthieu's last commit.	Pierre Letouzey	2015-04-10
\| *	Eauto hints respect their priority. Fixes bug #3199.	Pierre-Marie Pédrot	2015-04-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Fixing bug #3298.	Pierre-Marie Pédrot	2015-02-26
* \|	Less compatibility layer in Eauto.	Pierre-Marie Pédrot	2015-02-23
* \|	Partially porting eauto to the new tactic API.	Pierre-Marie Pédrot	2015-02-23
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.	Hugo Herbelin	2014-12-07
*	Fixing side bug in db37c9f3f32ae7 delaying interpretation of the	Hugo Herbelin	2014-11-16
*	Remaining tactics of the Auto module were put in the monad.	Pierre-Marie Pédrot	2014-10-15
*	A version of convert_concl and convert_hyp in new proof engine.	Hugo Herbelin	2014-10-09
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Fixing bug #2810 (autounfold on local variable declared as hint but cleared).	Hugo Herbelin	2014-10-02
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15
*	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin	2014-09-10
*	Tactics.unify in the new monad.	Pierre-Marie Pédrot	2014-08-23
*	Reorganization of tactics:	Hugo Herbelin	2014-08-18
*	Correct eauto which was not dealing properly with polymorphic constants.	Matthieu Sozeau	2014-07-21
*	Properly refresh the local hintdb database in case an external tactic changed	Matthieu Sozeau	2014-06-26
*	Clenvtac.unify is in the new monad.	Pierre-Marie Pédrot	2014-06-23
*	Oops, I fixed the .ml's	Matthieu Sozeau	2014-06-23
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	Passing some tactics to the new monad type.	Pierre-Marie Pédrot	2014-06-12
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12