coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
*	Monotonizing the Evarutil module.	Pierre-Marie Pédrot	2016-02-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.	Maxime Dénès	2016-01-15
* \|	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
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\\| \|
\| * \|	Extraction: msg_notice instead of msg_info.	Pierre Courtieu	2016-01-04
* \| \|	Fix typos.	Guillaume Melquiond	2016-01-01
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \|
* \| \|	Simplifying code of fourier.	Hugo Herbelin	2015-12-30
* \| \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \| \|	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
* \| \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\| * \|	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
* \| \|	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
\| \|/ \|/\|
* \|	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-17
\|\\|
\| *	Extraction: slightly better heuristic for Obj.magic simplifications	Pierre Letouzey	2015-12-16
\| *	Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplifications	Pierre Letouzey	2015-12-16
\| *	Extraction: more cautious use of intermediate result caching (fix #3923)	Pierre Letouzey	2015-12-15
\| *	Extraction: fix a few little glitches with my last commit (replacing unused v...	Pierre Letouzey	2015-12-15
\| *	Extraction: replace unused variable names by _ in funs and matchs (fix #2842)	Pierre Letouzey	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-15
\|\\|
\| *	Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)	Pierre Letouzey	2015-12-14
\| *	Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)	Pierre Letouzey	2015-12-14
\| *	Extraction: cosmetically avoid generating spaces on empty lines	Pierre Letouzey	2015-12-14
\| *	Extraction: also get rid of explicit '\n' for haskell	Pierre Letouzey	2015-12-14
\| *	Extraction: fix a pretty-print issue	Pierre Letouzey	2015-12-14
\| *	Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")	Pierre Letouzey	2015-12-14
\| *	Extraction: nicer implementation of Implicits	Pierre Letouzey	2015-12-12
\| *	Extraction: check for remaining implicits after dead code removal (fix #4243)	Pierre Letouzey	2015-12-12
\| *	Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)	Pierre Letouzey	2015-12-12
\| *	Extraction: avoid generating some blanks at end-of-line	Pierre Letouzey	2015-12-12
* \|	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
* \|	Getting rid of dynamic hacks in Setoid_newring.	Pierre-Marie Pédrot	2015-12-04
* \|	Removing the last use of tacticIn in setoid_ring.	Pierre-Marie Pédrot	2015-12-03