coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Prevent a useless evar normalization in Clenvtac.unify.	Pierre-Marie Pédrot	2016-06-20
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	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
* \|	Removing uselessly duplicated function in Evd.	Pierre-Marie Pédrot	2015-09-27
\|/
*	Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...	Pierre-Marie Pédrot	2015-05-18
*	Update headers.	Maxime Dénès	2015-01-12
*	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
*	Add support for deactivating type class inference from induction/destruct.	Hugo Herbelin	2014-10-13
*	Revert "While resolving typeclass evars in clenv, touch only the ones that ap...	Matthieu Sozeau	2014-09-17
*	While resolving typeclass evars in clenv, touch only the ones that appear in the	Matthieu Sozeau	2014-09-17
*	While we don't have a clean alternative to Clenvtac, add a primitive	Matthieu Sozeau	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
*	Putting implicit arguments of Clenv.res_pf right.	Pierre-Marie Pédrot	2014-06-25
*	Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it	Pierre-Marie Pédrot	2014-06-24
*	Clenvtac.res_pf is in the new tactic monad.	Pierre-Marie Pédrot	2014-06-24
*	Clenvtac.unify is in the new monad.	Pierre-Marie Pédrot	2014-06-23
*	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau	2014-05-06
*	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
*	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot	2014-04-22
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Backtrack on unneeded change of interface for pose_metas_as_evars.	msozeau	2013-06-04
*	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau	2013-06-04
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Monomorphization (proof)	ppedrot	2012-11-25
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Added a flag to control the use of typing when instantiating applied	herbelin	2011-12-17
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10