coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
*	Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...	Jason Gross	2018-04-12
\|\
* \	Merge PR #500: Move bugs that have been closed on Bugzilla	Maxime Dénès	2018-04-12
\|\ \
* \ \	Merge PR #7087: Congruence tactic engine update	Pierre-Marie Pédrot	2018-04-12
\|\ \ \
\| \| * \|	Fix the status of some resolved bugs	Tej Chajed	2018-04-11
\| \|/ / \|/\| \|
* \| \|	Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...	Emilio Jesus Gallego Arias	2018-04-09
\|\ \ \
* \ \ \	Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation	Pierre-Marie Pédrot	2018-04-09
\|\ \ \ \
* \ \ \ \	Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)	Maxime Dénès	2018-04-09
\|\ \ \ \ \
\| \| * \| \| \|	Fix #6956: Uncaught exception in bytecode compilation	Maxime Dénès	2018-04-06
* \| \| \| \| \|	Improve shell scripts	zapashcanon	2018-04-05
\| \| \| \| \| *	Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.	Théo Zimmermann	2018-04-05
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.	Hugo Herbelin	2018-04-04
\|\ \ \ \ \ \| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6407: Fix #6404 - Print tactics called by ML tactics	Pierre-Marie Pédrot	2018-04-04
\|\ \ \ \ \
\| \| \| * \| \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	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 #6257: anomaly with Printing Projections and Context.	Gaëtan Gilbert	2018-03-30
\| \| \| * \|	Fixes #7110 ("as" untested while looking for notation for nested patterns).	Hugo Herbelin	2018-03-29
* \| \| \| \|	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
\| \| \|/ /
\| \| \| *	Congruence: Fixing a bug with native projections.	Hugo Herbelin	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
\|\ \ \ \ \ \ \ \