coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
*	Merge PR #6599: Decimals in prelude	Maxime Dénès	2018-02-24
\|\
* \	Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès	2018-02-21
\|\ \
\| \| *	Add CHANGES entry for decimals in prelude	Jason Gross	2018-02-20
* \| \|	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin	2018-02-20
* \| \|	More flexibility in locating or referring to a notation.	Hugo Herbelin	2018-02-20
* \| \|	A first step at refreshing and documenting the new feature.	Hugo Herbelin	2018-02-20
* \| \|	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
\| \|/ \|/\|
\| *	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
* \|	CHANGES for 8.7.2.	Théo Zimmermann	2018-02-14
\|/
*	Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)	Maxime Dénès	2018-02-14
\|\
\| *	Add CHANGES entry for #1047	Tej Chajed	2018-02-13
* \|	CHANGES for universe variance	Gaëtan Gilbert	2018-02-12
\|/
*	Merge PR #6629: Archive COMPATIBILITY	Maxime Dénès	2018-01-23
\|\
\| *	Move the mention of the removal of Qed exporting at the right place.	Théo Zimmermann	2018-01-22
* \|	Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.	Maxime Dénès	2018-01-22
\|\ \
* \| \|	add flash infos about wrap, not found, no. of replacements, no. of finds, iss...	Paul Steckler	2018-01-18
\| \|/ \|/\|
* \|	Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.	Maxime Dénès	2018-01-18
\|\ \
\| \| *	Add CHANGES entry	Jasper Hugunin	2018-01-17
\| * \|	Add CHANGES entry	Jasper Hugunin	2018-01-17
\| \|/
* \|	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\ \ \| \|/ \|/\|
\| *	Documentation and CHANGES for bracket with goal selector.	Théo Zimmermann	2018-01-05
* \|	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
\|/
*	Merge PR #6377: Removal of the FAQ LaTex document.	Maxime Dénès	2017-12-20
\|\
* \	Merge PR #6381: A version of [time] that works on constr evaluation	Maxime Dénès	2017-12-18
\|\ \
* \ \	Merge PR #6380: Add tactics to reset and display the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \
* \ \ \	Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...	Maxime Dénès	2017-12-18
\|\ \ \ \
\| \| \| \| *	Removing the FAQ, which has been moved to the GitHub wiki for this	Matt Quinn	2017-12-18
* \| \| \| \|	Merge PR #6429: 8.7.1 CHANGES.	Maxime Dénès	2017-12-15
\|\ \ \ \ \
\| \| \| \| * \|	Add documentation for time_constr	Jason Gross	2017-12-14
\| \| \| \|/ /
\| \| \| * /	Add doc+changelog entries for new LtacProf tactics	Jason Gross	2017-12-14
\| \|_\|/ / \|/\| \| \|
\| * \| \|	8.7.1 CHANGES.	Théo Zimmermann	2017-12-14
* \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\|/ / /
* \| \|	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès	2017-12-07
\|\ \ \
\| \| * \|	use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language	Paul Steckler	2017-12-05
\| \|/ / \|/\| \|
* \| \|	Update CHANGES	Matthieu Sozeau	2017-12-01
\| \|/ \|/\|
* \|	Merge PR #6276: Coqchk accepts filenames	Maxime Dénès	2017-12-01
\|\ \
* \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| * \|	Documenting the possibility to pass filenames to coqchk.	Pierre-Marie Pédrot	2017-11-29
\|/ /
\| *	Selecting which notation to print based on current stack of scope.	Hugo Herbelin	2017-11-27
\|/
*	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
*	Moving bug numbers to BZ# format in the CHANGES file.	Théo Zimmermann	2017-10-19
*	Merge PR #540: [configure] Support for flambda flags.	Maxime Dénès	2017-10-10
\|\
* \	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\ \
\| \| *	[configure] Support for flambda flags.	Emilio Jesus Gallego Arias	2017-10-10
\| \|/ \|/\|
* \|	Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...	Maxime Dénès	2017-10-09
\|\ \
* \| \|	8.7+beta2 CHANGES	Théo Zimmermann	2017-10-06
\| \| *	romega: takes advantage of context variables with body	Pierre Letouzey	2017-10-05
\| \| *	Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...	Pierre Letouzey	2017-10-05
\| \|/ \|/\|
* \|	Mention requiring extraction/funind in CHANGES	Tej Chajed	2017-10-02