coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
\| *	Fix a bug preventing the generation of graphs when doing multiple	Matthieu Sozeau	2015-11-18
* \|	Preventing an unwanted warning 5 "this function application is partial"	Hugo Herbelin	2015-11-07
* \|	Merge remote-tracking branch 'origin/v8.5' into upstream-trunk	Hugo Herbelin	2015-11-07
\|\\|
\| *	Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan	Hugo Herbelin	2015-11-06
* \|	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
* \|	Proofview.Goal.sigma returns an indexed evarmap.	Pierre-Marie Pédrot	2015-10-20
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	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
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	f_equal fix continued: do a refresh_universes as before.	Matthieu Sozeau	2015-10-08
\| *	Fix bug #4069: f_equal regression.	Matthieu Sozeau	2015-10-07