coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
* \|	Fixing some problems with double induction.	Hugo Herbelin	2016-01-21
* \|	Code simplification in elim.ml.	Hugo Herbelin	2016-01-20
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Moving is_quantified_hypothesis to new proof engine.	Hugo Herbelin	2016-01-14
* \|	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
\|/
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Removing tactic compatibility layer from Elim.	Pierre-Marie Pédrot	2014-04-22
*	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot	2014-04-22
*	Define Tactics.bring_hyps in the new monad.	Pierre-Marie Pédrot	2014-03-28
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Fixing pervasive equalities. In particular, I removed the code that deleted	Pierre-Marie Pédrot	2014-03-03
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-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
*	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Modulification of identifier	ppedrot	2012-12-14
*	still some more dead code removal	letouzey	2012-10-06
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30