| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross | |
| This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. | |||
| 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. | |||
| 2015-07-26 | Regenerate the axiom figure of the FAQ. | Guillaume Melquiond | |
| 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. | |||
| 2015-07-26 | Remove obsolete question about eta-conversion. | Guillaume Melquiond | |
| 2015-07-22 | Refman: document Show Universes. | Matthieu Sozeau | |
| 2015-07-22 | Remove obsolete documentation. (Fix bug #4238) | Guillaume Melquiond | |
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-08 | Fix documentation of universes. | Matthieu Sozeau | |
| 2015-07-08 | Fix documentation. | Guillaume Melquiond | |
| 2015-07-07 | Document Set/Print Firstorder Solver option. | Matthieu Sozeau | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-26 | 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 | |
| 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. | |||
| 2015-06-26 | Added _CoqProject to the index of the reference manual. | Assia Mahboubi | |
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-17 | Doc: Workers do check for guardedness before sending proofs back | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |