coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv	Matej Kosik	2015-12-17
*	ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_conv	Matej Kosik	2015-12-17
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
*	CLEANUP: in the Reductionops module	Matej Kosik	2015-12-17
*	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
*	Getting rid of some hardwired generic arguments.	Pierre-Marie Pédrot	2015-12-17
*	Fixing e3cefca41b about supposingly simplifying primitive projections	Hugo Herbelin	2015-12-15
*	Fixing unexpected length of context in a typing function, detected by	Hugo Herbelin	2015-12-15
*	Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.	Hugo Herbelin	2015-12-15
*	API: documenting context_chop and removing a duplicate.	Hugo Herbelin	2015-12-15
*	Adding a token "index" representing positions (1st, 2nd, etc.).	Hugo Herbelin	2015-12-15
*	Simplifying documentation of "assert form as pat".	Hugo Herbelin	2015-12-15
*	Granting clear_flag in injection, even legacy mode. This is possible	Hugo Herbelin	2015-12-15
*	Tactics: Generalizing the use of the experimental clearing modifier to	Hugo Herbelin	2015-12-15
*	Revert "Revert PMP's fix of #2498, which introduces an incompatibility with l...	Pierre-Marie Pédrot	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
\| *	Fixing little bug of coq_makefile with unterminated comment.	Hugo Herbelin	2015-12-14
\| *	extraction_impl.v: fix a typo	Pierre Letouzey	2015-12-14
\| *	A test file for Extraction Implicit (including bugs #4243 and #4228)	Pierre Letouzey	2015-12-14
\| *	Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)	Pierre Letouzey	2015-12-14
* \|	Adding compatibility flag for 8.5.	Hugo Herbelin	2015-12-14
\| *	Fix \label which was meants to be \ref in doc of CIC terms.	Maxime Dénès	2015-12-14
\| *	Remove a mention of Set Virtual Machine in doc.	Maxime Dénès	2015-12-14
\| *	CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' message	Enrico Tassi	2015-12-14
\| *	Updating CHANGES with an incompatibility.	Hugo Herbelin	2015-12-14
\| *	Revert PMP's fix of #2498, which introduces an incompatibility with lablgtk	Maxime Dénès	2015-12-14
\| *	Flag -compat 8.4 now loads Coq.Compat.Coq84.	Maxime Dénès	2015-12-14
\| *	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès	2015-12-14
\| *	Test file for #4363 was not complete.	Maxime Dénès	2015-12-14
\| *	Extraction: cosmetically avoid generating spaces on empty lines	Pierre Letouzey	2015-12-14
* \|	Remove some occurrences of Unix.opendir.	Guillaume Melquiond	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
* \|	More code sharing between tactic notation and genarg interpretation.	Pierre-Marie Pédrot	2015-12-13
\| *	Extraction: documentation of the new option Unset Extraction SafeImplicits	Pierre Letouzey	2015-12-12
\| *	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
* \|	Removing dead unsafe code in Genarg.	Pierre-Marie Pédrot	2015-12-12
\| *	Indexing and documenting some options.	Pierre-Marie Pédrot	2015-12-12
\| *	Optimize occur_evar_upto_types, avoiding repeateadly looking into the	Matthieu Sozeau	2015-12-11
\| *	Univs: Fix bug #4363, nested abstract.	Matthieu Sozeau	2015-12-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	Document removal of Set Virtual Machine and -vm in CHANGES.	Maxime Dénès	2015-12-11
\| *	Remove Set Virtual Machine from doc, since the command itself has been removed.	Maxime Dénès	2015-12-11
\| *	Add tactic native_cast_no_check, analog to vm_cast_no_check.	Maxime Dénès	2015-12-11
\| *	Fixing a pat%constr bug. Thanks to Enrico for reporting.	Hugo Herbelin	2015-12-10