coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \|	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
\| \|/
* /	[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