coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
*	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès	2017-11-21
\|\
* \	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès	2017-11-20
\|\ \
\| \| *	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
\| \|/ \|/\|
* \|	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\| *	Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.	Hugo Herbelin	2017-11-08
* \|	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\|/
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
* \|	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
* \|	Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).	Hugo Herbelin	2017-10-05
\| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \|	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias	2017-09-20
\| *	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| *	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\|/
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès	2017-08-31
\|\
\| *	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin	2017-08-29
* \|	Remove understand_tcc_evars.	Maxime Dénès	2017-08-01
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[vernac] Remove forward hooks from Obligations.	Emilio Jesus Gallego Arias	2017-06-20
*	[vernac] Remove unused hooks.	Emilio Jesus Gallego Arias	2017-06-20
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Fix bugs	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Change the place of inference after sect discharge	Amin Timany	2017-06-16
*	Subtyping inference for inductoves and records	Amin Timany	2017-06-16
*	Add subtyping inference for inductive types	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	Extend definition of inductives to include subtyping info	Amin Timany	2017-06-16
*	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias	2017-06-11
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...	Maxime Dénès	2017-06-06
\|\
* \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \|	Merge PR#696: Trunk+cleanup constr of global	Maxime Dénès	2017-06-01
\|\ \
* \ \	Merge PR#561: Improving the Name API	Maxime Dénès	2017-06-01
\|\ \ \
\| * \| \|	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
\| \| \| *	More precise on preventing clash between bound vars name and hidden impargs.	Hugo Herbelin	2017-05-31
\| \| \| *	Fixing a failure to interpret some local implicit arguments in Inductive.	Hugo Herbelin	2017-05-31
\| \| \|/ \| \|/\|
* / \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\|/ /
\| *	Command.ml cleanup: remove constr_of_global calls	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] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\
\| * \	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\| \|\ \
\| \| \| *	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| \| \|/ \| \|/\|