| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-12 | Merge PR #963: fix coq_makefile | Maxime Dénès | |
| 2017-08-12 | Add some things Jason mentioned | Tej Chajed | |
| 2017-08-12 | Expand PR process explanation | Tej Chajed | |
| 2017-08-12 | Link to the existing list of tutorials | Tej Chajed | |
| 2017-08-12 | fix coq_makefile | Matej Košík | |
| Make sure that when plugin writer does not use -bypass-API, API is opened by default. | |||
| 2017-08-12 | More portable location for the time command. | Théo Zimmermann | |
| On NixOS in particular, /usr/bin/time doesn't exist. | |||
| 2017-08-11 | Introducing a syntax for goal dispatch. | Pierre-Marie Pédrot | |
| 2017-08-10 | Simplify a bit of wording | Tej Chajed | |
| 2017-08-10 | Describe pull requests a bit more precisely | Tej Chajed | |
| 2017-08-10 | Some more tweaks to contributing guide | Tej Chajed | |
| 2017-08-10 | Amendments to contributing doc | Tej Chajed | |
| Incorporating some feedback from @Zimmi48 | |||
| 2017-08-10 | Add a set of contributing guidelines | Tej Chajed | |
| Heavily inspired by the Rust guidelines (https://github.com/rust-lang/rust/blob/master/CONTRIBUTING.md). | |||
| 2017-08-08 | Another batch of primitive operations. | Pierre-Marie Pédrot | |
| 2017-08-08 | Set detachable windows type hint to dialog. | Olivier Marty | |
| Windows such as Search & Replace are dialogs. For some window managers, the hint changes how the window is displayed. | |||
| 2017-08-08 | Code simplification in quotations. | Pierre-Marie Pédrot | |
| 2017-08-07 | Defining several aliases for built-in tactics. | Pierre-Marie Pédrot | |
| 2017-08-07 | Defining abbreviations for tactics that can parse as atoms. | Pierre-Marie Pédrot | |
| 2017-08-07 | Fix location of not-unit warning. | Pierre-Marie Pédrot | |
| 2017-08-07 | Fix parsing of parenthesized expressions. | Pierre-Marie Pédrot | |
| 2017-08-07 | Defining a few base tacticals. | Pierre-Marie Pédrot | |
| 2017-08-07 | Introducing grammar-free tactic notations. | Pierre-Marie Pédrot | |
| 2017-08-07 | Add build_coq_or to API | Sigurd Schneider | |
| 2017-08-06 | Print names of all open blocks | Tej Chajed | |
| Fixes bug 5597. | |||
| 2017-08-05 | Exporting more reduction functions. | Pierre-Marie Pédrot | |
| 2017-08-05 | More notations for basic tactics. | Pierre-Marie Pédrot | |
| 2017-08-05 | Exporting the rewrite tactic. | Pierre-Marie Pédrot | |
| 2017-08-04 | Introducing quotations for the rewrite tactic. | Pierre-Marie Pédrot | |
| 2017-08-04 | Makefile: install-byte works even if -coqide no | Enrico Tassi | |
| 2017-08-04 | Adding locations to quotation types. | Pierre-Marie Pédrot | |
| 2017-08-04 | More precise type for quoted structures. | Pierre-Marie Pédrot | |
| 2017-08-04 | Adding the induction and destruct tactics. | Pierre-Marie Pédrot | |
| 2017-08-04 | Introducing notations for destruct and induction arguments. | Pierre-Marie Pédrot | |
| 2017-08-03 | Amend wording to capture intended meaning | Sam Pablo Kuper | |
| per @Zimmi48's comments [here](https://github.com/coq/coq/pull/944#discussion_r131072333) and [here](https://github.com/coq/coq/pull/944#discussion_r131072790). | |||
| 2017-08-02 | Inserting enter functions in Ltac1 bindings. | Pierre-Marie Pédrot | |
| 2017-08-02 | Tentatively implementing apply. | Pierre-Marie Pédrot | |
| 2017-08-02 | Typo in documentation. | Pierre-Marie Pédrot | |
| 2017-08-02 | Expanding documentation. | Pierre-Marie Pédrot | |
| 2017-08-02 | Fix compilation of horrible Ltac2 example. | Pierre-Marie Pédrot | |
| 2017-08-02 | Properly implementing the notation to easily access hypotheses. | Pierre-Marie Pédrot | |
| 2017-08-02 | Code factorization in elim notation. | Pierre-Marie Pédrot | |
| 2017-08-02 | Merging the e/- variants of primitive tactics. | Pierre-Marie Pédrot | |
| 2017-08-02 | Rewording the introduction | Enrico Tassi | |
| The contents should be exactly the same. I removed the distinction between tactical and pseudo-tactical because I think that it is too much technical for the introduction. I used "syntactic construction" and made appeal to the reader intuition by saying that such construction behaves similarly to a tactical. I think the text would be much more readable if "the tactics described in Chapter..." could be replaced by a *name*, but I'm afraid the only one I could use (Ltac) is a bit too ambiguous. So I'm open to suggestions. | |||
| 2017-08-02 | Rephrasing a couple of sentences in a more factual way. | Hugo Herbelin | |
| 2017-08-02 | Rephrasing the introduction in a more factual and up-to-date way. | Hugo Herbelin | |
| 2017-08-02 | Port ssr manual to Coq's latex/hevea style | Enrico Tassi | |
| Work done by Assia Mahboubi and Enrico Tassi | |||
| 2017-08-02 | Makefile.doc: implement serve-refman-8080 target | Enrico Tassi | |
| We make it so that, by default, the HTML reference manual looks like the one published online (same .css) and we provide a target to serve it locally (requires python). | |||
| 2017-08-02 | Adding new notations. | Pierre-Marie Pédrot | |
| 2017-08-02 | Extending the set of tactic scopes. | Pierre-Marie Pédrot | |
| We now allow mere tokens, keywords and sequencing amongst others. | |||
| 2017-08-02 | Update Setoid.tex | larsr | |
| The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`. | |||
| 2017-08-02 | More examples | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |