coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6407: Fix #6404 - Print tactics called by ML tactics	Pierre-Marie Pédrot	2018-04-04
\|\
* \|	Update coq_makefile timing test	Jason Gross	2018-04-02
\| *	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
\|/
*	Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)	Pierre-Marie Pédrot	2018-04-01
\|\
* \|	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
* \|	Fix #6631: Derive Plugin gives "Anomaly: more than one statement".	Pierre-Marie Pédrot	2018-03-29
\| *	Supporting fix/cofix in Ltac pattern-matching (wish #7092).	Hugo Herbelin	2018-03-28
* \|	Merge PR #7090: stm: don't propagate side effects when editing a proof	Emilio Jesus Gallego Arias	2018-03-28
\|\ \
* \ \	Merge PR #6961: [test-suite] Add backtracking test for `Load`.	Enrico Tassi	2018-03-28
\|\ \ \
\| \| * \|	stm: don't propagate side effects when editing a proof	Enrico Tassi	2018-03-27
\| \| \|/
* \| /	Slightly refining some error messages about unresolvable evars.	Hugo Herbelin	2018-03-24
\| \|/ \|/\|
\| *	[test-suite] Add backtracking test for `Load`.	Emilio Jesus Gallego Arias	2018-03-10
\|/
*	Merge PR #6946: Fix expected number of arguments for cumulative constructors.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...	Maxime Dénès	2018-03-09
\|\ \
\| \| *	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
\|\ \
\| \| *	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès	2018-03-09
\| \|/ \|/\|
\| *	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	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
* \|	Merge PR #6480: Allow Prop as source for coercions	Maxime Dénès	2018-03-09
\|\ \ \| \|/ \|/\|
* \|	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès	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 #6945: Fix error with univ binders on monomorphic records.	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6155: Get rid of ' notation for Zpos in QArith	Maxime Dénès	2018-03-09
\|\ \ \
* \ \ \	Merge PR #6747: Relax conversion of constructors according to the pCuIC model	Maxime Dénès	2018-03-09
\|\ \ \ \
* \ \ \ \	Merge PR #6328: Fix #6313: lost goals in nested ltac in refine	Maxime Dénès	2018-03-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values	Maxime Dénès	2018-03-09
\|\ \ \ \ \ \
\| \| * \| \| \| \|	More examples about shelve/given_up in tactic-in-terms.	Hugo Herbelin	2018-03-08
\| \| * \| \| \| \|	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6522: Fix core hint database issue #6521	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	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
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| *	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Fix error with univ binders on monomorphic records.	Gaëtan Gilbert	2018-03-08
\| \| \| \| * \| \| \|	Fix SR breakage due to allowing fixpoints on non-rec values	Matthieu Sozeau	2018-03-08
\| \| \| \| \| * \| \|	Add test-suite file for cumulative constructors	Matthieu Sozeau	2018-03-08
\| \| \| \| \| \| \|/ \| \| \| \| \| \|/\|
* \| \| \| \| \| \|	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6903: [compat] Remove "Shrink Abstract"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \|	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \