coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Merge PR #6767: [ci] add elpi	Maxime Dénès	2018-02-21
\|\
* \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| *	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\|/
*	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...	Maxime Dénès	2018-02-19
\|\
\| *	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
* \|	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \| \|/ \|/\|
* \|	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
* \|	Delete duplicate line	Paul Steckler	2018-01-30
\| *	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/
*	Remove dead code from funind.	Maxime Dénès	2018-01-24
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	[API] remove large file containing duplicate interfaces	Enrico Tassi	2017-12-27
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
*	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\
* \	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \
\| \| *	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| *	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
\| \|/
\| *	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
* \|	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \| \|/ \|/\|
\| *	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
* \|	Getting rid of pf_is_matching in Funind.	Pierre-Marie Pédrot	2017-12-06
\|/
*	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
*	Use Entries.constant_universes_entry more.	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
*	[api] Deprecate Term destructors, move to Constr	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 #6181: [proof] Attempt to deprecate some V82 parts of the proof API.	Maxime Dénès	2017-11-21
\|\
* \|	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias	2017-11-19
\| *	[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
*	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
*	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
*	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
*	Merge PR #1040: Efficient fresh name generation	Maxime Dénès	2017-10-03
\|\
* \|	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
\| *	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\|/
*	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
*	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès	2017-08-16
\|\
* \	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \
\| \| *	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
\| \|/ \|/\|
* \|	Merge PR #806: closing bug 5315	Maxime Dénès	2017-08-01
\|\ \
\| \| *	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
* \| \|	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \ \ \| \|_\|/ \|/\| \|
\| \| *	closing bug 5315	Julien Forest	2017-07-29
\| \|/ \|/\|
\| *	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27