coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\
\| *	fixing bug 4609: document an option governing the generation of equalities	Yves Bertot	2016-10-03
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-02
\| \|\
\| \| *	Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.	Hugo Herbelin	2016-09-30
\| * \|	Merge branch 'v8.5' into v8.6	Maxime Dénès	2016-09-30
\| \|\\|
\| \| *	Fix a bug in subst releaved by an OCaml warning.	Maxime Dénès	2016-09-29
* \| \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \| \| \|	CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function	Matej Kosik	2016-08-25
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Remove extraneous dot in error message (bug #4832).	Guillaume Melquiond	2016-08-19
\| \| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| \| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| \|/ \|/\|
* \|	Fixing #3070 ("subst" taking properly into account chains of dependencies).	Hugo Herbelin	2016-08-17
* \|	Disallow dependent case on prim records w/o eta	Matthieu Sozeau	2016-07-06
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Make semantics of whd_zeta consistent with other whd_* functions.	Maxime Dénès	2016-07-01
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
* \|	Optmimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
* \|	Optimization in the subst tactic.	Pierre-Marie Pédrot	2016-06-24
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \|	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
* \|	Removing the old refine tactic from the Tactics module.	Pierre-Marie Pédrot	2016-05-17
* \|	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	In Regular Subst Tactic mode, ensure that the order of hypotheses is	Hugo Herbelin	2016-05-03
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-09
\|\\|
\| *	Fix strategy of Keyed Unification	Matthieu Sozeau	2016-03-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
* \|	Exporting build_selector, a component of discriminate, for use in congruence.	Hugo Herbelin	2016-03-05
\| *	Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...	Matthieu Sozeau	2016-02-23
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	Code factorization of tactic "unfold_body".	Pierre-Marie Pédrot	2016-02-15
* \| \|	Moving conversion functions to the new tactic API.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
\| *	Fix essential bug in new Keyed Unification mode reported by R. Krebbers.	Matthieu Sozeau	2016-01-12
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Fixing an "injection as" bug in the presence of side conditions.	Hugo Herbelin	2015-12-25
\|/ /
* \|	Granting clear_flag in injection, even legacy mode. This is possible	Hugo Herbelin	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	More optimizations of [Clenv.clenv_fchain].	Pierre-Marie Pédrot	2015-11-17
* \|	Removing some goal unsafeness in Equality.	Pierre-Marie Pédrot	2015-10-29
* \|	Removing the evar_map argument from s_enter.	Pierre-Marie Pédrot	2015-10-29