coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\|
*	Fixed doc of fresh (was already outdated before fixing #3233).	Pierre Courtieu	2015-02-23
\|
*	Remove Whelp commands.	Maxime Dénès	2015-02-17
\| \| \| \| \| \|	Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
*	Separate index for vernacular options.	Maxime Dénès	2015-02-17
\|
*	Remove documentation of non-existing Show Implicits command.	Maxime Dénès	2015-02-17
\|
*	Remove non-existing Tactic Definition command from index.	Maxime Dénès	2015-02-17
\|
*	Fix sentence that was cut in doc of Local Set.	Maxime Dénès	2015-02-17
\|
*	Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.	Hugo Herbelin	2015-02-16
\|
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
\| \| \| \|	Of course such proofs cannot be processed asynchronously
*	dependent destruction: Fix (part of) bug #3961, by fixing dependent *	Matthieu Sozeau	2015-02-14
\| \| \| \|	generalizing * which was broken since 8.4.
*	Fix typos about .vio files (thanks Arthur for spotting them)	Enrico Tassi	2015-02-12
\|
*	Make clearer that "Remove Printing Let" does not influence destructuring let.	Guillaume Melquiond	2015-02-12
\|
*	Avoid html markup inside tex files and fix url.	Guillaume Melquiond	2015-02-10
\|
*	A few refinements in whodidwhat 8.4.	Hugo Herbelin	2015-02-10
\|
*	Add section numbering to the refman PDF. (Fix for bug #2365)	Guillaume Melquiond	2015-02-10
\|
*	Prevent Latex from messing with backticks. (Fix for bug #3871)	Guillaume Melquiond	2015-02-10
\|
*	Fix documentation of generalize. (Fix for bug #4015)	Guillaume Melquiond	2015-02-10
\|
*	Fix some documentation typo.	Guillaume Melquiond	2015-02-10
\|
*	Fix some documentation typos.	Guillaume Melquiond	2015-02-05
\|
*	Fix index of reference manual.	Guillaume Melquiond	2015-01-29
\|
*	Remove spurious "Loading ML file" and "<W> Grammar extension" from the ↵	Guillaume Melquiond	2015-01-29
\| \| \| \|	reference manual.
*	Remove some "Warning:" from the reference manual.	Guillaume Melquiond	2015-01-29
\|
*	Fix some typos in the documentation.	Guillaume Melquiond	2015-01-29
\|
*	Fix some broken Coq scripts in the reference manual.	Guillaume Melquiond	2015-01-29
\|
*	Doc: Overfull lines in chapter on Canonical Structures.	Hugo Herbelin	2015-01-27
\|
*	Doc: Fixing some compilation problems with chapter Canonical	Hugo Herbelin	2015-01-24
\| \| \| \| \|	Structures. Text mode + a "Require Import" in a module which provokes suspect warnings "Exception Not_found".
*	Reference Manual: Documenting new printing of evars and new effect of	Hugo Herbelin	2015-01-24
\| \| \| \|	Set Printing Existential Instances (see bug report #3951).
*	Reference Manual/Credits: expand the paragraph on the new proof engine to ↵	Arnaud Spiwack	2015-01-21
\| \| \| \|	match the overall style.