coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès	2017-08-16
\|\
* \	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \
\| \| *	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
\| \|/ \|/\|
* \|	Merge PR #806: closing bug 5315	Maxime Dénès	2017-08-01
\|\ \
\| \| *	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
* \| \|	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \ \ \| \|_\|/ \|/\| \|
\| \| *	closing bug 5315	Julien Forest	2017-07-29
\| \|/ \|/\|
\| *	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
* \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\|/
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[funind] Remove spurious character in comment.	Emilio Jesus Gallego Arias	2017-07-17
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
*	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
*	Safer API for Global.body_of_constant and variants.	Pierre-Marie Pédrot	2017-07-13
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	closing bug #5618 introduce by PR 828	Julien Forest	2017-06-29
*	closing bug #4250	Julien Forest	2017-06-23
*	Merge PR#803: Clean ssr	Maxime Dénès	2017-06-20
\|\
\| *	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\|/
*	Merge PR#763: [proof] Deprecate redundant wrappers.	Maxime Dénès	2017-06-14
\|\
* \	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \
* \| \|	Recdef do now a Require Export FunInd (better compat)	Pierre Letouzey	2017-06-14
* \| \|	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
* \| \|	Merge PR#718: API cleanup: aliases	Maxime Dénès	2017-06-12
\|\ \ \
\| \| \| *	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias	2017-06-11
\| \|_\|/ \|/\| \|
* \| \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| * \|	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
\|/ /
\| *	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\|/
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge PR#716: Don't double up on periods in anomalies	Maxime Dénès	2017-06-06
\|\
* \	Merge PR#722: [printing] Remove duplicated printing function.	Maxime Dénès	2017-06-05
\|\ \
* \ \	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès	2017-06-05
\|\ \ \
\| \| \| *	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \| \| \|	solving implicit resolution in Function	Julien Forest	2017-06-01
\| \|_\|/ \|/\| \|
* \| \|	Merge PR#696: Trunk+cleanup constr of global	Maxime Dénès	2017-06-01
\|\ \ \
\| \| \| *	[printing] Remove duplicated printing function.	Emilio Jesus Gallego Arias	2017-06-01
\| \| * \|	Renaming allow_patvar flag of intern_gen into pattern_mode.	Hugo Herbelin	2017-05-31
\| \| \|/
* \| /	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
\| \|/ \|/\|
\| *	Cleanup: removal of constr_of_global.	Matthieu Sozeau	2017-05-29
\|/
*	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\
\| *	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27