coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Elim API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Hipattern API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacticals API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	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