coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Fixing printing of Function.	Hugo Herbelin	2016-04-27
* \| \|	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
* \| \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \| \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \| \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \ \
* \| \| \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
* \| \| \|	More conversion functions in the new tactic API.	Pierre-Marie Pédrot	2016-02-15
* \| \| \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
\| * \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ / /
* \| \|	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
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \
\| * \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \| \|	Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.	Pierre-Marie Pédrot	2015-12-28
* \| \| \|	Tentative API fix for tactic arguments to be fed to tclWITHHOLES.	Pierre-Marie Pédrot	2015-12-27
\|/ / /
* \| \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\| \|
\| * \|	Fix some typos.	Guillaume Melquiond	2015-12-07
* \| \|	Removing redundant versions of generalize.	Hugo Herbelin	2015-12-05
* \| \|	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\| \|
\| * \|	Fix a bug preventing the generation of graphs when doing multiple	Matthieu Sozeau	2015-11-18
* \| \|	Monotonizing Tactics.change_arg.	Pierre-Marie Pédrot	2015-10-29
* \| \|	Removing some goal unsafeness in inductive schemes.	Pierre-Marie Pédrot	2015-10-29
* \| \|	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
\| * \|	Univs: fix bug #4375, accept universe binders on (co)-fixpoints	Matthieu Sozeau	2015-10-28
\| * \|	Do not pause globing in funind. (Fix bug #4382)	Guillaume Melquiond	2015-10-28
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\| \|
* \| \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \| \|	Function debug mode more formatted.	Pierre Courtieu	2015-10-19
\| * \|	Partly fixes #3225. Removed some old experimental stuff in funind.	Pierre Courtieu	2015-10-19
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\| \|
\| * \|	Fix some typos.	Guillaume Melquiond	2015-10-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\| \|
\| * \|	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau	2015-10-02
\| * \|	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau	2015-10-02
\| \| *	Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...	Arnaud Spiwack	2015-09-25
* \| \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\| \|
\| * \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
\| \| *	Add corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
\| \|/ \|/\|
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13