coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\
\| *	Fixes to compile with ocaml 4.01	Matthieu Sozeau	2016-11-07
\| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
* \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \|	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \|/ \|/\|
\| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| *	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\
\| *	Allow to unset the refinement mode of Instance in ML	Matthieu Sozeau	2016-04-07
* \|	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
* \|	Moving Refine to its proper module.	Pierre-Marie Pédrot	2016-03-20
* \|	Typeclasses: respect Declare Instance priority	Matthieu Sozeau	2016-03-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\\|
\| *	Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.	Pierre-Marie Pédrot	2016-02-19
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Allow program hooks to see the refined universe_context at the end of a	Matthieu Sozeau	2015-11-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: local names handling.	Matthieu Sozeau	2015-10-28
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
\|/
*	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
*	Hopefully better names to constructors of internal_flag, as discussed	Hugo Herbelin	2015-09-23
*	Fix declarations of instances to perform restriction of universe	Matthieu Sozeau	2015-04-09
*	Fix bug #4046.	Matthieu Sozeau	2015-02-18
*	Fix bug #3960: potential evar instance categorized as an unresolvable	Matthieu Sozeau	2015-02-16
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing bug #3632 for good.	Pierre-Marie Pédrot	2014-12-29
*	Adding a Refine Instance Mode option that allows to deactivate the	Pierre-Marie Pédrot	2014-11-30
*	Evd.future_goals: forgot to revert the list in two places.	Arnaud Spiwack	2014-10-23
*	Proofview: move more functions to the Unsafe module.	Arnaud Spiwack	2014-10-22
*	Remove the deprecated open-constr based refine.	Arnaud Spiwack	2014-10-22
*	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack	2014-10-22
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau	2014-09-15
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.	Matthieu Sozeau	2014-06-23
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18