coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge PR#793: Fixing restriction of existential variables regarding evar_store	Maxime Dénès	2017-06-20
\|\
* \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
* \|	Squashed commit of the following:	Amin Timany	2017-06-16
* \|	Check subtyping of inductive types in Kernel	Amin Timany	2017-06-16
* \|	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
* \|	New datastructure for universes of inductive types	Amin Timany	2017-06-16
\| *	Fixing restrict regarding evar_store.	Hugo Herbelin	2017-06-14
* \|	Deprecate options that were introduced for compatibility with 8.4.	Guillaume Melquiond	2017-06-14
* \|	Remove support for Coq 8.4.	Guillaume Melquiond	2017-06-14
\|/
*	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
* \|	Don't double up on periods in anomalies	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
\| \| \| *	Using EConstr and more invariants in record.ml.	Hugo Herbelin	2017-05-31
\| \| \|/ \| \|/\|
* / \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\|/ /
\| *	tactics 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] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Merge PR#655: Extra functions exported in EConstr	Maxime Dénès	2017-05-26
\|\
* \	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
\| \|/ /
\| * \|	Merge PR#518: Faster universe unification	Maxime Dénès	2017-05-23
\| \|\ \
\| \| \| *	Exporting some functions of vars.ml as functions operating on EConstr.	Hugo Herbelin	2017-05-19
\| \| \| *	In EConstr, defining some "cast" functions earlier.	Hugo Herbelin	2017-05-19
\| \| \| *	Moving "sym" on "eq" type to lib/util.ml.	Hugo Herbelin	2017-05-19
\| \| \|/ \| \|/\|
\| * \|	Merge PR#411: Mention template polymorphism in the documentation.	Maxime Dénès	2017-05-03
\| \|\ \
\| * \ \	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\ \ \
\| * \| \| \|	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
\| \| * \| \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| \| * \| \|	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \| * \| \|	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
\| \| * \| \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| \|/ / /
\| \| \| *	Fast path when checking equality of universe levels in UState.	Pierre-Marie Pédrot	2017-04-27
\| \| \| *	Code cleaning in unification algorithm for universes.	Pierre-Marie Pédrot	2017-04-27
\| \| \|/ \| \|/\|
\| * \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
* \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ /
* \|	"tclENV" is sexier, use it instead of "Env.get"	Matej Kosik	2017-04-20
* \|	reduce syntactic noise	Matej Kosik	2017-04-20
\| *	Update various comments to use "template polymorphism"	Gaetan Gilbert	2017-04-11
\|/
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
* \|	Restore a fast path in EConstr instance normalization.	Pierre-Marie Pédrot	2017-04-01
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
* \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01