coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès	2017-12-07
\|\
* \|	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
\| *	BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations	Paul Steckler	2017-09-25
\|/
*	Fix CHANGES after merge of PR #1025.	Théo Zimmermann	2017-09-15
*	read flags from project file for Compile Buffer	Paul Steckler	2017-09-05
*	move mention of native_compute profiling in CHANGES	Paul Steckler	2017-09-01
*	Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170	Maxime Dénès	2017-08-29
\|\
\| *	add CHANGES entry	Paul Steckler	2017-08-18
* \|	Correct the option for cumulativity in CHANGES	Amin Timany	2017-08-18
\|/
*	Use the wording suggested by Gaetan.	Théo Zimmermann	2017-08-17
*	Addition suggested by Pierre-Marie.	Théo Zimmermann	2017-08-17
*	Additions following Hugo's suggestions.	Théo Zimmermann	2017-08-16
*	Improve wording.	Théo Zimmermann	2017-08-16
*	8.7 CHANGES	Théo Zimmermann	2017-08-16
*	Porting #856 (8.6.1 CHANGES entries) to master	Théo Zimmermann	2017-08-16
*	Merge PR #925: Document Extraction TestCompile	Maxime Dénès	2017-08-01
\|\
\| *	Extraction TestCompile documented + mentionned in CHANGES	Pierre Letouzey	2017-07-27
* \|	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\|/
*	Add an entry to CHANGES about timing in coq_makefile	Jason Gross	2017-07-11
*	Update CHANGES with inversion_sigma entry	Jason Gross	2017-06-30
*	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\
\| *	[ide] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
* \|	Document cumulativity for inductive types	Amin Timany	2017-06-16
\|/
*	BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)	Pierre Letouzey	2017-06-13
*	Merge PR#709: Bytecode compilation apart from 'make world', again	Maxime Dénès	2017-06-12
\|\
\| *	mention 'make world' without 'byte' in CHANGES + 2 minor suggestions	Pierre Letouzey	2017-06-01
* \|	Merge PR#449: make specialize smarter (bug 5370).	Maxime Dénès	2017-06-01
\|\ \
\| * \|	Tests for new specialize feature + CHANGES.	Pierre Courtieu	2017-05-31
\| \|/
* /	Documentation for eassert, eenough, epose proof, eset, eremember, epose.	Hugo Herbelin	2017-05-30
\|/
*	Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings	Maxime Dénès	2017-05-25
\|\
* \	Merge PR#406: coq makefile2	Maxime Dénès	2017-05-25
\|\ \
\| * \|	enters coq_makefile2	Enrico Tassi	2017-05-23
* \| \|	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\|/ /
\| *	Clarifying the interpretation path for the "constr_with_binding" argument.	Hugo Herbelin	2017-05-22
\|/
*	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès	2017-05-17
\|\
* \|	Aligning on standard layout of CHANGES.	Hugo Herbelin	2017-05-13