coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	More conversion functions in the new tactic API.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fix bug #4537: Coq 8.5 is slower in typeclass resolution.	Pierre-Marie Pédrot	2016-01-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Remove duplicate definition.	Guillaume Melquiond	2016-01-02
\|/ /
* \|	Removing the evar_map argument from s_enter.	Pierre-Marie Pédrot	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
* \|	Renaming Goal.enter field into s_enter.	Pierre-Marie Pédrot	2015-10-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
* \|	Removing tclEVARS in various places.	Pierre-Marie Pédrot	2015-10-19
\| *	Generalize fix for auto from PMP to eauto and typeclasses eauto.	Matthieu Sozeau	2015-10-16
\|/
*	Fixing perfomance issue of auto hints induced by universes.	Pierre-Marie Pédrot	2015-10-14
*	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
*	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
*	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
*	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
*	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
*	Update headers.	Maxime Dénès	2015-01-12
*	Avoiding introducing yet another convention in naming files.	Hugo Herbelin	2015-01-08
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Follow up to experimental eager evar unification in bcba6d1bc9:	Hugo Herbelin	2014-11-08
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Remaining tactics of the Auto module were put in the monad.	Pierre-Marie Pédrot	2014-10-15
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Made Tacsubst independent of Auto at linking time so that Tacenv does	Hugo Herbelin	2014-10-01
*	Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.	Matthieu Sozeau	2014-09-27
*	Make pattern_of_constr typed so that we can infer the proper patterns	Matthieu Sozeau	2014-09-27
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau	2014-09-17
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin	2014-09-10
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
*	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot	2014-06-24
*	Less goal-entering.	Pierre-Marie Pédrot	2014-06-22
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	Improve hotspot in Auto.	Pierre-Marie Pédrot	2014-06-17
*	Passing some tactics to the new monad type.	Pierre-Marie Pédrot	2014-06-12
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing various backtrace recordings.	Pierre-Marie Pédrot	2014-04-25