coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	Remove unused lookup table.	Guillaume Melquiond	2014-04-28
*	Removing useless try-with clauses in Goal.enter variants.	Pierre-Marie Pédrot	2014-04-25
*	closing bug 3037	Julien Forest	2014-04-05
*	Using HMaps in global references.	Pierre-Marie Pédrot	2014-03-08
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Fixing some generic equalities in Micromega.	Pierre-Marie Pédrot	2014-03-03
*	Fixing Pervasives.equality in extraction.	Pierre-Marie Pédrot	2014-03-03
*	Getting rid of generic hashes in cc plugin.	Pierre-Marie Pédrot	2014-03-03
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Removing generic equality in Syntax plugin.	Pierre-Marie Pédrot	2014-03-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26
*	New compilation mode -vi2vo	Enrico Tassi	2014-02-26
*	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	fast correction of bug #3234	Julien Forest	2014-02-14
*	Less dependencies in Omega.	Pierre-Marie Pédrot	2014-02-08
*	Relaunch all Unix.waitpid when they ended with EINTR	Pierre Letouzey	2014-01-30
*	bug correction in proving principles of function	jforest	2014-01-20
*	Omega: avoiding distinct proof-terms on repeated identical runs	Pierre Letouzey	2014-01-10
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...	Frédéric Besson	2013-12-20
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Fix g_derive.ml4.	Arnaud Spiwack	2013-12-04
*	Derive plugin.	Arnaud Spiwack	2013-12-04
*	Factoring(continued).	Arnaud Spiwack	2013-12-04
*	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack	2013-12-04
*	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack	2013-12-04
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond	2013-12-03
*	Silence compilation warning by avoiding some deprecated constructs.	Guillaume Melquiond	2013-12-03
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Getting rid of goal-dependency in declarative mode argument evaluation.	Pierre-Marie Pédrot	2013-11-27
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Do not use ugly Dyn features in the Quote plugin. Use instead the	Pierre-Marie Pédrot	2013-11-26
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Field_theory: nicer notations for constants 0 1 ...	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
*	bugfix micromega: solved an ambiguous symbol resolution	fbesson	2013-11-15
*	Porting Tactics.assumption to the new engine.	ppedrot	2013-11-08
*	Fix congruence: normalise hypotheses with respect to evars.	aspiwack	2013-11-02
*	Made Proofview.Goal.hyps a named_context.	aspiwack	2013-11-02
*	Less use of the list-based interface for goal-bound tactics.	aspiwack	2013-11-02
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02