coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\
* \	Merge PR #6497: Add optimize_heap tactic for #6488	Maxime Dénès	2018-01-08
\|\ \
\| \| *	Brackets support single numbered goal selectors.	Théo Zimmermann	2018-01-05
\| \|/ \|/\|
\| *	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
* \|	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
* \|	Remove legacy Value.normalize function.	Maxime Dénès	2017-12-22
\|/
*	Merge PR #6381: A version of [time] that works on constr evaluation	Maxime Dénès	2017-12-18
\|\
* \	Merge PR #6406: Make [abstract] nodes show up in the Ltac profile	Maxime Dénès	2017-12-18
\|\ \
* \ \	Merge PR #6380: Add tactics to reset and display the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \
* \ \ \	Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording	Maxime Dénès	2017-12-18
\|\ \ \ \
* \ \ \ \	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\ \ \ \ \
\| * \| \| \| \|	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| \| \| * \|	Pass a ghost location for abstract	Jason Gross	2017-12-14
\| \| \| \| * \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| \| *	Add named timers to LtacProf	Jason Gross	2017-12-14
\| \| \| \|/
\| \| \| *	Add tactics to reset and display the Ltac profile	Jason Gross	2017-12-14
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6386: Catch errors while coercing 'and' intro patterns	Maxime Dénès	2017-12-14
\|\ \ \
* \ \ \	Merge PR #6379: Fix profiling plugin	Maxime Dénès	2017-12-14
\|\ \ \ \
* \ \ \ \	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Fix #5081 by more fine-grained LtacProf recording	Jason Gross	2017-12-12
\| \| \| \| \| \|/
\| \| \| * \| \|	Use msg_info for LtacProf	Jason Gross	2017-12-11
\| \| \| * \| \|	Allow LtacProf tactics to be called	Jason Gross	2017-12-11
\| \| \| \| \|/ \| \| \| \|/\|
\| \| \| \| *	Catch errors while coercing 'and' intro patterns	Tej Chajed	2017-12-11
\| \| \| \|/
* \| \| /	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|/ \|/\| \|
\| \| *	Remove deprecated appcontext and corresponding documentation.	Théo Zimmermann	2017-12-11
\| \| *	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \|/ \|/\|
\| *	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
* \|	[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
\| \|/