coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
*	[api] Misctypes removal: tactic flags.	Emilio Jesus Gallego Arias	2018-06-12
*	Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is provided	Matthieu Sozeau	2018-06-07
\|\
* \|	Remove some dead code in class_tactics.ml	Armaël Guéneau	2018-05-31
* \|	Merge PR #6969: [api] Remove functions deprecated in 8.8	Maxime Dénès	2018-05-31
\|\ \
* \| \|	Move interning the [hint_pattern] outside the Typeclasses hooks.	Gaëtan Gilbert	2018-05-30
\| * \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
\|/ /
\| *	Fix anomaly in autoapply when an unbound hint name is provided	Armaël Guéneau	2018-05-29
\|/
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	[api] Move `hint_info_expr` to `Typeclasses`.	Emilio Jesus Gallego Arias	2018-04-26
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	Add an invariant on given up goals in class_tactics.	Hugo Herbelin	2018-03-08
*	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
*	Proof engine: consider the pair principal and future goals as an entity.	Hugo Herbelin	2018-03-08
*	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\
* \	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \
\| \| *	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \|/ \|/\|
* \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \
\| * \|	[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
\| \|/
* /	proofview: goals come with a state	Enrico Tassi	2018-02-20
\|/
*	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
*	Cleanup name-binding structure for fresh evar name generation.	Pierre-Marie Pédrot	2018-01-02
*	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	Merge PR #805: Functional tactics	Maxime Dénès	2017-08-29
\|\
* \	Merge PR #919: Remove a few useless evar-normalizations in printing code.	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
\|\ \ \
\| \| \| *	env, sigma as first arguments of functions	amblaf	2017-07-31
\| \| \| *	Remove references to Global.env in tactics/*.ml	amblaf	2017-07-31
\| \|_\|/ \|/\| \|
\| * \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| *	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot	2017-07-26
\| \|/ \|/\|
* \|	Merge PR #868: Fix debug trace of typeclasses eauto.	Maxime Dénès	2017-07-26
\|\ \ \| \|/ \|/\|
* \|	Merge PR #892: Improve do_split option of typeclass resolution	Maxime Dénès	2017-07-20
\|\ \
* \ \	Merge PR #869: Enforce alternating separators in typeclass debug output	Maxime Dénès	2017-07-20
\|\ \ \
\| \| \| *	Fix debug trace of typeclasses eauto.	Théo Zimmermann	2017-07-19
\| \| * \|	Improve do_split option of typeclass resolution	Matthieu Sozeau	2017-07-18
\| \| \|/
\| * /	format pairs of items for pr_depth to get alternating separators	Paul Steckler	2017-07-12
\| \|/
* /	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological	Maxime Dénès	2017-06-19
\|\
* \	Merge PR#727: [tactics] Fix summary registration of global hint variable.	Maxime Dénès	2017-06-19
\|\ \
\| \| *	[typeclasses eauto] Fix bug #3943: non-termination in topological	Matthieu Sozeau	2017-06-14
* \| \|	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot	2017-06-13
\| \|/ \|/\|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\ \
* \| \|	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
* \| \|	Merge PR#638: Fix bug #5360: anomalies in typeclass resolution output	Maxime Dénès	2017-06-06
\|\ \ \
\| \| \| *	[tactics] Fix summary registration of global hint variable.	Emilio Jesus Gallego Arias	2017-06-03
\| \|_\|/ \|/\| \|
\| \| *	Fix bug 5550: "typeclasses eauto with" does not work with section variables.	Théo Zimmermann	2017-05-30