coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
*	Using the same type of binders for interning and externing.	Hugo Herbelin	2017-03-24
*	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
*	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
*	Merging glob_binder and glob_decl.	Hugo Herbelin	2017-03-24
*	Type extended_glob_local_binder now contains only glob_constr.	Hugo Herbelin	2017-03-24
*	Standardized the order of constructors for binders: Assum then Def.	Hugo Herbelin	2017-03-24
*	Cleaning phase around local binder at glob level:	Hugo Herbelin	2017-03-24
*	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin	2017-03-24
*	Merge PR#392: strengthened the statement of JMeq_eq_dep	Maxime Dénès	2017-03-24
\|\
* \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-24
\|\ \
\| * \	Merge PR#476: [future] Be eager when "chaining" already resolved future values.	Maxime Dénès	2017-03-24
\| \|\ \
\| * \ \	Merge PR#475: Opaque side effects	Maxime Dénès	2017-03-24
\| \|\ \ \
* \| \ \ \	Merge PR#504: [META] add support for ide libraries	Maxime Dénès	2017-03-24
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#503: make check not CoqIDE-specific	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#433: doc: fix a French-ism	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \ \ \ \| \| \|_\|_\|/ / / / \| \|/\| \| \| \| \| \|
\| * \| \| \| \| \| \|	Merge PR#507: Intern names bound in match patterns	Maxime Dénès	2017-03-23
\| \|\ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	Documenting the API of side-effects.	Pierre-Marie Pédrot	2017-03-23
\| \| \| \| \| \| * \| \|	Using a dedicated datastructure for side effect ordering.	Pierre-Marie Pédrot	2017-03-23
\| \| \| \| \| \| * \| \|	Making the side_effects type opaque.	Pierre-Marie Pédrot	2017-03-23
\| \| \|_\|_\|_\|/ / / \| \|/\| \| \| \| \| \|
\| \| * \| \| \| \| \|	Intern names bound in match patterns	Tej Chajed	2017-03-23
* \| \| \| \| \| \| \|	Merge PR#501: [travis] Fix iris-coq build.	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \ \ \ \ \ \ \| \| \|/ / / / / / / \| \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.	Maxime Dénès	2017-03-23
\| \|\ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \|	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès	2017-03-23
* \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Merge PR#495: funind: Ignore missing info for current function	Maxime Dénès	2017-03-23
\| \|\ \ \ \ \ \ \ \ \ \| \| \|_\|_\|/ / / / / / \| \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès	2017-03-23
\| * \| \| \| \| \| \| \| \|	Merge PR#491: Do not typecheck twice the type of opaque constants.	Maxime Dénès	2017-03-23
\| \|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \|	[META] add support for ide libraries	Emilio Jesus Gallego Arias	2017-03-23
\| * \| \| \| \| \| \| \| \| \|	Merge PR#480: show unused intro pattern warning	Maxime Dénès	2017-03-22
\| \|\ \ \ \ \ \ \ \ \ \
* \| \ \ \ \ \ \ \ \ \ \	Merge PR#493: [safe-string] update dev/doc/changes	Maxime Dénès	2017-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#415: Use a compact representation for real literals	Maxime Dénès	2017-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \|	make check not CoqIDE-specific	Paul Steckler	2017-03-22
\| \| \| \| \| \| \| \| \| \| \|/ / /
* \| \| \| \| \| \| \| \| \| / / /	Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.	Hugo Herbelin	2017-03-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \|	[travis] Fix iris-coq build.	Emilio Jesus Gallego Arias	2017-03-22
\| \|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Document the changes to IZR.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Make IZR a morphism for field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Mark ring morphisms as opaque.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
\| \| \| \| \| \| \| * \| \| \|	[travis] [8.6.only] Backport latest changes from trunk.	Emilio Jesus Gallego Arias	2017-03-22
\| \| \| \| \|_\|_\|/ / / / \| \| \| \|/\| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Make IZR use a compact representation of integers.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \|	Fix broken evaluation strategies for ring and field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \|	Fix some typos.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \|	Simplify some proofs using ring and field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \|	Remove duplicate lemmas.	Guillaume Melquiond	2017-03-22
\|/ / / / / / / / /
\| \| \| \| \| * / / /	funind: Ignore missing info for current function	Tej Chajed	2017-03-22
\| \| \| \|_\|/ / / / \| \| \|/\| \| \| \| \|
* \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-03-22
\|\ \ \ \ \ \ \ \ \| \| \|/ / / / / / \| \|/\| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR#390: Updates to the Pretty Printing Infrastructure	Maxime Dénès	2017-03-22
\|\ \ \ \ \ \ \ \