coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6754: Better elaboration of pattern-matchings on primitive projections	Pierre-Marie Pédrot	2018-06-19
\|\
\| *	Add test-suite case for performance, had to use Timeout	Matthieu Sozeau	2018-06-15
\| *	Better elaboration of pattern-matchings on primitive projections	Matthieu Sozeau	2018-06-15
* \|	Do not allow spliting in res_pf, this is reserved for pretyping	Matthieu Sozeau	2018-06-15
\|/
*	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\
* \	Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.	Matthieu Sozeau	2018-06-04
\|\ \
\| \| *	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| \|/ \|/\|
* \|	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
* \|	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
* \|	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
* \|	Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.	Hugo Herbelin	2018-04-26
* \|	Merge PR #7237: [ssr] fix delayed clears (fix #7045)	Maxime Dénès	2018-04-16
\|\ \
* \| \|	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
\| * \|	[ssr] fix delayed clears (fix #7045)	Enrico Tassi	2018-04-13
\|/ /
* \|	Merge PR #7087: Congruence tactic engine update	Pierre-Marie Pédrot	2018-04-12
\|\ \
* \| \|	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\| \| *	Fix #6770: fixpoint loses locality info in proof mode.	Gaëtan Gilbert	2018-03-29
\| \|/ \|/\|
\| *	Congruence: Fixing a bug with native projections.	Hugo Herbelin	2018-03-27
\|/
*	Fix expected number of arguments for cumulative constructors.	Gaëtan Gilbert	2018-03-09
*	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\
\| *	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
\| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
* \|	added test for coercion from type	charguer	2018-03-09
* \|	allow Prop as source for coercions	charguer	2018-03-09
\|/
*	Merge PR #6747: Relax conversion of constructors according to the pCuIC model	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6522: Fix core hint database issue #6521	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...	Maxime Dénès	2018-03-08
\|\ \ \
\| \| \| *	Add test-suite file for cumulative constructors	Matthieu Sozeau	2018-03-08
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \
\| \| * \|	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
* \| \| \|	[compat] Remove "Shrink Abstract"	Emilio Jesus Gallego Arias	2018-03-06
* \| \| \|	Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...	Maxime Dénès	2018-03-06
\|\ \ \ \
* \ \ \ \	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \| * \| \| \| \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \| \|/ / / / /
* \| \| \| \| \| \|	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	Adding a test file for evar handling in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \|_\|_\|/ / \| \|/\| \| \| \|
* / \| \| \| \|	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
\|/ / / / /
\| * / / /	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/ / / /
* \| \| \|	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin	2018-02-20
* \| \| \|	Notations: Do not consider a non-occurring variable as a binder-only variable.	Hugo Herbelin	2018-02-20
\| \| * \|	Implement name mangling option	Jasper Hugunin	2018-02-17
* \| \| \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \|/ / \|/\| \|
\| * \|	Fixing an anomaly in the presence of "let-in" in the type of a record.	Hugo Herbelin	2018-02-13
\|/ /
* \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
* \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
* \|	Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.	Maxime Dénès	2018-01-18
\|\ \
\| * \|	Add a test that `prod_applist_assum` reduces the right number of let-ins	Jasper Hugunin	2018-01-17