coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	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
* \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\|/
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[funind] Remove spurious character in comment.	Emilio Jesus Gallego Arias	2017-07-17
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
*	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
*	Safer API for Global.body_of_constant and variants.	Pierre-Marie Pédrot	2017-07-13
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	closing bug #5618 introduce by PR 828	Julien Forest	2017-06-29
*	closing bug #4250	Julien Forest	2017-06-23
*	Merge PR#803: Clean ssr	Maxime Dénès	2017-06-20
\|\
\| *	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\|/
*	Merge PR#763: [proof] Deprecate redundant wrappers.	Maxime Dénès	2017-06-14
\|\
* \	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \
* \| \|	Recdef do now a Require Export FunInd (better compat)	Pierre Letouzey	2017-06-14