coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| \| *	In enter_one, not having exactly one goal is a fatal error of the monad.	Hugo Herbelin	2017-06-23
\| \|/ \|/\|
* \|	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
* \| \| \|	Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...	Maxime Dénès	2017-06-06
\|\ \ \ \
\| \| \| * \|	Univs: fix bug #5365, generation of u+k <= v constraints	Matthieu Sozeau	2017-06-05
* \| \| \| \|	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
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Bump year in headers.	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