coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\
* \	Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...	Maxime Dénès	2017-10-06
\|\ \
* \ \	Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...	Maxime Dénès	2017-10-05
\|\ \ \
* \ \ \	Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...	Maxime Dénès	2017-10-05
\|\ \ \ \
\| \| \| * \|	Fixing BZ#5769 (variable of type "_something" was named after invalid "_").	Hugo Herbelin	2017-10-05
\| \| \| \| *	Remove TODO comment (Evar.t is opaque)	Gaëtan Gilbert	2017-09-29
\| \| \| \|/
* \| \| \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
* \| \| \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| \|_\|/ \|/\| \|
\| \| *	Moving setting of "cleared" evar flag directly in Evd.restrict.	Hugo Herbelin	2017-09-27
\| \| *	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
\| \|/ \|/\|
\| *	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \	Merge PR #1036: Unify EConstr.t equality	Maxime Dénès	2017-09-19
\|\ \
\| \| *	Document UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| *	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| *	proof_global: cleanup and comment close_proof	Matthieu Sozeau	2017-09-19
\| \| *	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\| \|/ \|/\|
* \|	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond	2017-09-12
\| *	Normalizing universes before performing term comparison.	Pierre-Marie Pédrot	2017-09-08
\| *	Using EConstr equality check in unification.	Pierre-Marie Pédrot	2017-09-08
\|/
*	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\
* \	Merge PR #913: Less allocations in Detyping	Maxime Dénès	2017-08-01
\|\ \
* \ \	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \ \
\| * \| \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
* \| \| \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\|/ / /
\| * /	No useless reallocation in Termops.collapse_appl.	Pierre-Marie Pédrot	2017-07-21
\|/ /
* \|	[proofs] Remove circular dependency from Proofview to Goal.	Emilio Jesus Gallego Arias	2017-07-19
* \|	Merge PR #781: Remove dead code [Universes.simplify_universe_context]	Maxime Dénès	2017-07-17
\|\ \
* \| \|	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
* \| \|	Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel	Maxime Dénès	2017-07-13
\|\ \ \
\| * \| \|	Less footguns in universe handling: remove subst_instance_context.	Pierre-Marie Pédrot	2017-07-11
\| * \| \|	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
* \| \| \|	Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...	Maxime Dénès	2017-07-07
\|\ \ \ \ \| \|/ / / \|/\| \| \|
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\ \ \ \
* \| \| \| \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| \| \| \| *	Adding intermediate entry point to create an evar in empty rel_context.	Hugo Herbelin	2017-06-25
\| \|_\|_\|/ \|/\| \| \|
\| \| * \|	In enter_one, not having exactly one goal is a fatal error of the monad.	Hugo Herbelin	2017-06-23
\| \|/ / \|/\| \|
\| \| *	Remove dead code [Universes.simplify_universe_context]	Gaëtan Gilbert	2017-06-20
\| \|/ \|/\|
* \|	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
\| \| *	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \| \|\
\| \| * \	Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints	Maxime Dénès	2017-06-15
\| \| \|\ \
\| * \| \| \|	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