coq - The formal proof system

Age	Commit message (Collapse)	Author
2015-11-10	Merge origin/v8.5 into trunk	Hugo Herbelin
	Did some manual merge in tactics/tactics.ml.
2015-11-07	Adding an amazing property of Prop.	Hugo Herbelin

2015-11-07	Fixing documention of Add Printing Coercion.	Hugo Herbelin

2015-11-05	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-11-04	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau

2015-11-04	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau
	inconsistent).
2015-10-19	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-18	Reference Manual: Applying standard style recommendation about not	Hugo Herbelin
	starting a sentence with a symbolic expression.
2015-10-15	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-14	Fix some typos.	Guillaume Melquiond

2015-10-13	Fix some typos.	Guillaume Melquiond

2015-10-12	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-11	Documenting matching under binders.	Hugo Herbelin

2015-10-10	Fix a few latex errors in documentation of Proof Using (e.g. \tt*).	Guillaume Melquiond

2015-10-09	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-08	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi
	- "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems.
2015-10-06	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-04	Fix typo. (Fix bug #4355)	Guillaume Melquiond

2015-10-02	Mark the Coq.Compat files for documentation. (Fix bug #4353)	Guillaume Melquiond

2015-10-02	Fixing error messages about Hint.	Hugo Herbelin

2015-10-02	Improving reference manual in that auto uses simple apply rather than apply.	Hugo Herbelin
	Still, there are small differences, e.g. on "use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some amount of use of delta that Matthieu would know better than me if it matters or not in practice.
2015-10-02	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-09-30	Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).	Hugo Herbelin
	Incidentally made writing style in CoqIDE chapter more homogeneous.
2015-09-28	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond
	This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq.
2015-09-26	Documenting how to support some special unicode characters in coqdoc	Hugo Herbelin
	(thanks to coq-club, Sep 2015).
2015-09-26	Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.	Hugo Herbelin

2015-09-25	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-09-25	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot

2015-09-25	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot

2015-09-21	Fixing tutorial.	Pierre-Marie Pédrot
	The V7 to V8 translator lost part of term annotations.
2015-09-13	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-09-10	typo in refman.	Pierre Courtieu

2015-09-08	Documenting the new behaviour of the Shrink Obligations flag.	Pierre-Marie Pédrot

2015-08-22	Documenting the Shrink Abstract option.	Pierre-Marie Pédrot

2015-08-22	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-08-17	Remove generatable documentation files from repository. (Fix bug #4315)	Guillaume Melquiond

2015-08-05	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-08-02	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin
	considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v.
2015-07-31	Fix typos in the Extraction part of the reference manual.	Guillaume Melquiond
	In particular, fix the name of all the user contributions.
2015-07-31	Fix typos in the Micromega part of the reference manual.	Guillaume Melquiond

2015-07-31	Improve the table of content of the reference manual.	Guillaume Melquiond
	Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts.
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond

2015-07-30	Avoid suggesting elim and decompose in the FAQ.	Guillaume Melquiond

2015-07-30	Remove some output of Qed in the FAQ.	Guillaume Melquiond

2015-07-30	Fix some broken Coq scripts in the documentation.	Guillaume Melquiond

2015-07-29	Improve the FAQ a bit.	Guillaume Melquiond

2015-07-29	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-07-28	Reset a dangling proof in the FAQ.	Guillaume Melquiond

2015-07-27	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-07-27	search: Add an output-name-only search option	Clément Pit--Claudel
	When set, search results only display symbol names, instead of displaying full terms with types. This is useful when the list of symbols is needed by an external program, in particular for doing completion in IDEs.