coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
*	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\
* \	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\ \
\| \| *	Make set minimization option internal to Universes	Gaëtan Gilbert	2018-05-17
\| \|/ \|/\|
* \|	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
\| *	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
\|/
*	Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.	Hugo Herbelin	2018-04-26
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \
\| * \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
* \| \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ /
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
*	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\
\| *	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
* \|	Cleanup name-binding structure for fresh evar name generation.	Pierre-Marie Pédrot	2018-01-02
\|/
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25
\| *	Use Maps and ids for universe binders	Gaëtan Gilbert	2017-11-24
\|/
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\
* \|	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
* \|	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
* \|	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès	2017-09-15
\|\ \
\| * \|	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond	2017-09-12
* \| \|	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\|/ /
* \|	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
\| *	Fixing another regression with 8.4 wrt to βι-normalization of created hyps.	Hugo Herbelin	2017-08-21
* \|	Remove understand_tcc_evars.	Maxime Dénès	2017-08-01
* \|	Move type_uconstr to Tacinterp.	Maxime Dénès	2017-08-01
* \|	Remove understand_judgment and understand_judgment_tcc.	Maxime Dénès	2017-08-01
* \|	Remove allow_anonymous_refs.	Maxime Dénès	2017-08-01
* \|	Remove pure_open_constr (now open_constr)	Maxime Dénès	2017-08-01
* \|	Move glob_constr_ltac_closure to evar_refiner.	Maxime Dénès	2017-08-01
\|/
*	closing bug 5315	Julien Forest	2017-07-29
*	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge PR#716: Don't double up on periods in anomalies	Maxime Dénès	2017-06-06
\|\
* \	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès	2017-06-05
\|\ \