coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\
\| *	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin	2015-08-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v.
\| *	Fix typos in the Extraction part of the reference manual.	Guillaume Melquiond	2015-07-31
\| \| \| \| \| \| \| \|	In particular, fix the name of all the user contributions.
\| *	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	2015-07-31
\| \| \| \| \| \| \| \| \| \|	Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts.
\| *	Remove some outdated files and fix permissions.	Guillaume Melquiond	2015-07-31
\| \|
\| *	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-30
\| \|
\| *	Improve the FAQ a bit.	Guillaume Melquiond	2015-07-29
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-29
\|\\|
\| *	Reset a dangling proof in the FAQ.	Guillaume Melquiond	2015-07-28
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
* \|	search: Add an output-name-only search option	Clément Pit--Claudel	2015-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| *	Regenerate the axiom figure of the FAQ.	Guillaume Melquiond	2015-07-26
\| \| \| \| \| \| \| \| \| \| \| \|	The .png was ugly (less than 400px wide) and did not match the content of the .fig file (e.g. presence of '$'). To improve things a bit, text is now rendered by latex.
\| *	Remove obsolete question about eta-conversion.	Guillaume Melquiond	2015-07-26
\| \|
\| *	Refman: document Show Universes.	Matthieu Sozeau	2015-07-22
\| \|
\| *	Remove obsolete documentation. (Fix bug #4238)	Guillaume Melquiond	2015-07-22
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\|
\| *	Fix documentation of universes.	Matthieu Sozeau	2015-07-08
\| \|
\| *	Fix documentation.	Guillaume Melquiond	2015-07-08
\| \|
\| *	Document Set/Print Firstorder Solver option.	Matthieu Sozeau	2015-07-07
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
\| \|
\| *	Typos in my previous edition of the reference manual.	Assia Mahboubi	2015-06-26
\| \|
\| *	Some edition in the coq_makefile/_CoqProject section.	Assia Mahboubi	2015-06-26
\| \| \| \| \| \| \| \| \| \| \| \|	There are still two items I do not undertand fully (the last one about -extra-phony, and the removal of external libraries at make clean time, that I could not reproduce on a toy example.
\| *	Added _CoqProject to the index of the reference manual.	Assia Mahboubi	2015-06-26
\| \|
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Doc: Workers do check for guardedness before sending proofs back	Enrico Tassi	2015-06-17
\| \|
* \|	Turning "Set Regular Subst Tactic" on by default (for 8.6).	Hugo Herbelin	2015-05-15
\|/
*	Documenting Set Regular Subst Tactic (though unsure this is worth the	Hugo Herbelin	2015-05-13
\| \| \| \| \|	level of details, and this option should certainly disappear eventually).
*	Documenting the Loose Hint Behavior flag.	Pierre-Marie Pédrot	2015-05-13
\|
*	Fix documentation of Redirect	Enrico Tassi	2015-05-04
\|
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
\| \| \| \| \| \| \|	The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
*	Fixing a few typos + some uniformization of writing in doc.	Hugo Herbelin	2015-04-17
\|
*	Documenting the recommandation of toplevel-only commands.	Pierre-Marie Pédrot	2015-04-15
\|
*	Fix compilation of documentation broken by the addition of MMapAVL.	Guillaume Melquiond	2015-04-02
\|
*	Make sure that hyperref creates the proper links to the documentation indexes.	Guillaume Melquiond	2015-04-02
\|
*	Fix documentation of -R and -Q.	Guillaume Melquiond	2015-04-02
\|
*	Fixing a few typos + some uniformization of writing in doc.	Hugo Herbelin	2015-04-01
\|
*	More clarifications on loadpaths.	Pierre-Marie Pédrot	2015-04-01
\|
*	Documenting "From * Require *" and clearing a bit the loadpath chapter.	Pierre-Marie Pédrot	2015-04-01
\|
*	Fix various typos in documentation	Matěj Grabovský	2015-03-31
\| \| \| \|	Closes #57.
*	Qed export -> Qed exporting	Enrico Tassi	2015-03-22
\|
*	Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107)	Guillaume Melquiond	2015-03-21
\|
*	Fixing #4127 (command for locating exists notation in refman changed).	Hugo Herbelin	2015-03-13
\|
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
*	Preprend Fail to all the expected failures in the documentation.	Guillaume Melquiond	2015-03-05
\| \| \| \| \| \| \|	This commit also removes comments from Coq examples, as they cause extraneous delayed prompts that clutter the output because coq_tex cannot remove them. Some documentation errors were also fixed in the process, since they are easier to spot now that only unexpected failures stand out.
*	Typos in doc modules.	Hugo Herbelin	2015-03-03
\|
*	Fixing bug 3099.	Pierre-Marie Pédrot	2015-02-26
\|