coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	Use Evarutil.has_undefined_evars for tactic has_evar.	Gaëtan Gilbert	2017-11-24
\| *	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| *	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\|/
*	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\
* \	Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Maxime Dénès	2017-11-23
\|\ \
\| \| *	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
\| \|/ \|/\|
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
* \|	Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses	Maxime Dénès	2017-11-21
\|\ \
\| * \|	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin	2017-11-20
\| \| *	Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Gaëtan Gilbert	2017-11-19
\| \|/ \|/\|
\| *	Fixing printing of tactics encapsulated as tacarg with Tacexp.	Hugo Herbelin	2017-11-15
\| *	Using "l" printer for glob_constr, like for constr.	Hugo Herbelin	2017-11-15
* \|	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\|/
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
\| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
* \|	Adding support for syntax "let _ := e in e'" in Ltac.	Hugo Herbelin	2017-11-04
\|/
*	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\
* \	Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).	Maxime Dénès	2017-11-03
\|\ \
\| \| *	Ltac Debug: exporting env and sigma when needed so that term can be printed.	Hugo Herbelin	2017-11-02
\| \| *	Binding ltac printing functions to the system of generic printing.	Hugo Herbelin	2017-11-02
\| \| *	Setting a system to register printers for Ltac values.	Hugo Herbelin	2017-11-02
\| \| *	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\| \| *	Exporting a few more printing functions.	Hugo Herbelin	2017-11-02
\| \| *	Improving checks about the list separator in tactic notations.	Hugo Herbelin	2017-11-02
\| \|/ \|/\|
\| *	Fixing #2881 ("change with" failing in an Ltac definition).	Hugo Herbelin	2017-10-30
* \|	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès	2017-10-27
\|\ \
* \ \	Merge PR #677: Trunk+abstracting injection flags	Maxime Dénès	2017-10-27
\|\ \ \ \| \|_\|/ \|/\| \|
\| * \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| \| *	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\| \|/
* /	Typo in comment in tactic_matching.ml.	Hugo Herbelin	2017-10-24
\|/
*	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
*	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias	2017-10-10
*	Merge PR #1087: [stm] Switch to a functional API	Maxime Dénès	2017-10-09
\|\
* \	Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...	Maxime Dénès	2017-10-09
\|\ \
* \ \	Merge PR #1114: Generic handling of nameable objects for plugins	Maxime Dénès	2017-10-09
\|\ \ \
\| \| \| *	[stm] Switch to a functional API	Emilio Jesus Gallego Arias	2017-10-06
\| \|_\|/ \|/\| \|
\| \| *	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
\| \|/ \|/\|
* \|	Merge PR #1078: Report missing arguments in error message	Maxime Dénès	2017-10-04
\|\ \
\| \| *	Ltac uses the new generic locatable API.	Pierre-Marie Pédrot	2017-10-03
\| \| *	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot	2017-10-03
\| \|/ \|/\|
* \|	Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).	Maxime Dénès	2017-10-03
\|\ \
* \| \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
* \| \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\| * \|	Properly display the "only" prefix for selectors (bug #5760).	Guillaume Melquiond	2017-09-26
\| \| *	Report missing arguments in error message	Tej Chajed	2017-09-21
\| \|/
* \|	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
* \|	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\|/