coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[stm] Remove all but one use of VtUnknown.	Emilio Jesus Gallego Arias	2017-12-09
*	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\
* \	Merge PR #6210: More complete not-fully-applied error messages, #6145	Maxime Dénès	2017-12-05
\|\ \
\| * \|	more complete not-fully-applied error messages, #6145	Paul Steckler	2017-11-28
* \| \|	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
\|/ / /
\| \| *	Extending further PR#6047 (system to register printers for Ltac values).	Hugo Herbelin	2017-11-24
\| \| *	Printing again "intros **" as "intros" by default.	Hugo Herbelin	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
\|\ \