coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
*	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
\|/
*	[api] A few more minor deprecation notices.	Emilio Jesus Gallego Arias	2017-11-22
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
*	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
*	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
*	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès	2017-05-25
\|\
\| *	Generalizing the tactic-in-term embedding to any generic argument.	Pierre-Marie Pédrot	2017-05-03
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
\| *	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Cleaning up interfaces.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|/\|
\| *	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Fix bug #4723 and FIXME in API for solve_by_tac	Matthieu Sozeau	2016-09-28
* \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
* \|	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
\|/
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Allow `Pretyping.search_guard` to not check guard	Arnaud Spiwack	2016-06-15
* \|	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
* \|	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot	2016-03-25
* \|	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
* \|	Adding location to universes generated by the pretyper.	Pierre-Marie Pédrot	2016-02-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
* \| \|	Removing dynamic inclusion of constrs in tactic AST.	Pierre-Marie Pédrot	2015-12-04
\|/ /
* \|	Documenting a bit more interpretation functions in passing.	Hugo Herbelin	2015-10-26
* \|	Fixing #4221 (interpreting bound variables using ltac env was possibly	Hugo Herbelin	2015-08-02
\|/
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
*	Update headers.	Maxime Dénès	2015-01-12
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12