| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-16 | Merge PR #944: Fix typos. Improve wording. | Maxime Dénès | |
| 2017-08-16 | Merge PR #943: Reference Manual: minor wording improvements | Maxime Dénès | |
| 2017-08-16 | Merge PR #940: Replace jarring use of "Remark" with "Note" | Maxime Dénès | |
| 2017-08-16 | Merge PR #934: Fix some coq-tex errors in the reference manual. | Maxime Dénès | |
| 2017-08-16 | Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵ | Maxime Dénès | |
| wrongly tagged as keywords | |||
| 2017-08-16 | Merge PR #864: Some cleanups after cumulativity for inductive types | Maxime Dénès | |
| 2017-08-15 | Don't allow coq-dpdgraph to fail | Jason Gross | |
| 2017-08-15 | Move the rest of the ci target to a bash file | Jason Gross | |
| 2017-08-15 | Better error messages on the CI | Jason Gross | |
| This makes it so that when a ci target fails, we don't get red herring error messages about .ok files not existing. Since this requires bash, we make a helper script that invokes bash, so as to not depend on bash in general. | |||
| 2017-08-15 | Fix a typo | Jason Gross | |
| As per https://github.com/coq/coq/pull/968#discussion_r133238157 and https://github.com/coq/coq/pull/969#discussion_r133241472 | |||
| 2017-08-15 | Removing trailing "/" and "\" in directory names only on win32. | Hugo Herbelin | |
| This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows). | |||
| 2017-08-15 | Adding a test for BZ#1859 as suggested by @tchajed. | Théo Zimmermann | |
| 2017-08-15 | Never mind, don't mention coqdev | Tej Chajed | |
| I don't really want to recommend that someone subscribes to ask a question. | |||
| 2017-08-15 | Mention coqdev@ | Tej Chajed | |
| 2017-08-13 | Makefile : ignore user-contrib in various file searches | Pierre Letouzey | |
| This is crucial for the search for binary files without known sources (commit 7d1fc1), since coq_makefile currently doesn't install in user-contrib the ML sources of plugins. This could also helps for variables such as $(EXISTINGML). | |||
| 2017-08-12 | Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml. | Hugo Herbelin | |
| Indeed OCaml has a similar file and this conflicts, at least in debugger. | |||
| 2017-08-12 | Also mention Stack Exchange | Tej Chajed | |
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |