coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
*	Clarify the message "this hint will only be used by eauto"	Armaël Guéneau	2018-06-25
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Pierre-Marie Pédrot	2018-06-04
\|\
* \	Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...	Pierre-Marie Pédrot	2018-06-04
\|\ \
* \ \	Merge PR #7640: Small refactoring to clarify make_local_hint_db.	Pierre-Marie Pédrot	2018-06-04
\|\ \ \
\| \| * \|	Cleaning, documentation, uniformisation of the Coq extension of List.	Hugo Herbelin	2018-06-03
\| \|/ / \|/\| \|
* \| \|	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\ \ \
\| \| \| *	Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Armaël Guéneau	2018-05-31
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6969: [api] Remove functions deprecated in 8.8	Maxime Dénès	2018-05-31
\|\ \ \
\| \| * \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	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
\|/ /
* \|	Merge PR #7558: [api] Make `vernac/` self-contained.	Maxime Dénès	2018-05-30
\|\ \
\| \| *	Small refactoring to clarify make_local_hint_db.	Théo Zimmermann	2018-05-30
\| \|/ \|/\|
\| *	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
\| *	[tactics] Turn boolean locality hint parameter into a named one.	Emilio Jesus Gallego Arias	2018-05-27
* \|	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\|/
*	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
*	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	[api] Move `hint_info_expr` to `Typeclasses`.	Emilio Jesus Gallego Arias	2018-04-26
*	[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
\|\
* \|	[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
\|/
*	[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
*	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias	2017-11-19
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Better error messages, fix for BZ#5723	Paul Steckler	2017-09-11
*	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias	2017-06-11
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès	2017-05-25
\|\
* \	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
\| \|/ /
\| \| *	Allowing to pass arbitrary data in internalization environments.	Pierre-Marie Pédrot	2017-05-03
\| \|/
\| *	Remove unused module definition after merging PR#592.	Maxime Dénès	2017-05-02
\| *	Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.	Maxime Dénès	2017-05-02
\| \|\
\| \| *	Fix bug #5501: Universe polymorphism breaks proof involving auto.	Pierre-Marie Pédrot	2017-04-30
\| * \|	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| \|/
* /	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
\|/