coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tacinterp: fewer use of old-style goals.	Arnaud Spiwack	2013-11-25
*	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin	2013-11-25
*	Better implementation of summary unfreezing.	Pierre-Marie Pédrot	2013-11-24
*	Adding fold_left / fold_right function to maps.	Pierre-Marie Pédrot	2013-11-24
*	Updating new ftp link to old archives.	Hugo Herbelin	2013-11-24
*	Hardening the reading function of vo files.	Pierre-Marie Pédrot	2013-11-24
*	Slightly more efficient zip function in Closure.	Pierre-Marie Pédrot	2013-11-24
*	Tweaking arity & allocation of some basic functions.	Pierre-Marie Pédrot	2013-11-24
*	Small allocation improvement in Closure.	Pierre-Marie Pédrot	2013-11-23
*	configure: typo in my last commit	Pierre Letouzey	2013-11-23
*	Fixing bug #3165.	Pierre-Marie Pédrot	2013-11-23
*	Remove some occurrences of obsolete operators	Stephane Glondu	2013-11-22
*	configure: improve last fix	Pierre Letouzey	2013-11-22
*	Using hashes in Summary, like the previous commit did with Dyn.	Pierre-Marie Pédrot	2013-11-22
*	Using hashes instead of strings in dynamic tags. In case of collision, an	Pierre-Marie Pédrot	2013-11-22
*	configure: CAML_LD_LIBRARY_PATH is enriched, not overwritten	Pierre Letouzey	2013-11-21
*	configure: fix some issues with last commit	Pierre Letouzey	2013-11-21
*	Fix various \r issues with windows	Jason Gross	2013-11-21
*	Field_theory: nicer notations for constants 0 1 ...	Pierre Letouzey	2013-11-21
*	updated .mailmap	Pierre Letouzey	2013-11-21
*	Add Acc_intro_generator on top of all wf function proof (much much faster exe...	Julien Forest	2013-11-21
*	Adding Acc_intro_generator in order to help computations of Function in parti...	forest	2013-11-20
*	Optimization: in case of empty substitution, merging is trivial.	Pierre-Marie Pédrot	2013-11-19
*	update .mailmap with my email now that I've used it in a commit	Pierre Letouzey	2013-11-19
*	A .mailmap file for a nice git-shorlog display	Pierre Letouzey	2013-11-19
*	A file listing old svn branches and tags	letouzey	2013-11-18
*	Slightly faster version of merging substitutions in TacticMatching.	ppedrot	2013-11-16
*	Better implementation for stores.	ppedrot	2013-11-16
*	bugfix micromega: solved an ambiguous symbol resolution	fbesson	2013-11-15
*	Revert "Fast lookup_named in environments, based on maps instead of lists."	ppedrot	2013-11-15
*	Changes the semantics of Ltac's non-lazy pattern matching in presence of mult...	aspiwack	2013-11-14
*	Implementation of Ltac's match and match goal fully based on IStream.	aspiwack	2013-11-14
*	Update comments in matching.mli.	aspiwack	2013-11-14
*	Remove some dead code in tacinterp.	aspiwack	2013-11-14
*	Fast lookup_named in environments, based on maps instead of lists.	ppedrot	2013-11-13
*	Adding an unsafe mapping function to maps.	ppedrot	2013-11-13
*	Synchronizing the printer of tactic notations.	ppedrot	2013-11-13
*	Useless computation in Goal handle augmentation.	ppedrot	2013-11-12
*	Do not print tactic notation names at each interpretation step.	ppedrot	2013-11-12
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	Moving notation types into grammar rule.	ppedrot	2013-11-09
*	Cleaning and documenting Egramcoq.	ppedrot	2013-11-09
*	Partial applications in Goal.	ppedrot	2013-11-09
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Reverting the old LIFO behaviour of the notation finding algorithm.	ppedrot	2013-11-08
*	Removing partial applications in Reductionops.	ppedrot	2013-11-08
*	Useless array manipulation in Rtrees.	ppedrot	2013-11-08