coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-06-16	Using UInfoInd for universes in inductive types	Amin Timany
	It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
2017-06-16	Extend definition of inductives to include subtyping info	Amin Timany

2017-06-15	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès

2017-06-15	Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state	Maxime Dénès

2017-06-14	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	Merge PR#622: Change the default flag value for Refine.refine	Maxime Dénès

2017-06-14	API: exports Mltop.module_is_known to both API.mli and grammar_API.mli	Pierre Letouzey

2017-06-14	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey
	This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
2017-06-13	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot

2017-06-12	[lib] Remove obsolete state-management function add_frozen_state	Emilio Jesus Gallego Arias
	AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information.
2017-06-11	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias
	As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`.
2017-06-10	Remove (useless) aliases from the API.	Matej Košík

2017-06-09	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin
	Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
2017-06-07	Put "ssreflect" behind "API".	Matej Košík

2017-06-07	Put all plugins behind an "API".	Matej Kosik