| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-18 | Don't belittle the size of the SE community | Tej Chajed | |
| 2017-08-18 | Exporting scopes for occurrences. | Pierre-Marie Pédrot | |
| 2017-08-18 | Trying to enhance the printing of tactic expressions. | Pierre-Marie Pédrot | |
| 2017-08-18 | Separate jobs for test-suite and package building under OSX. | Maxime Dénès | |
| 2017-08-18 | Don't mention coq-club at all | Tej Chajed | |
| 2017-08-18 | Advise contributors to use SE over coq-club | Tej Chajed | |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler | |
| 2017-08-17 | Merge PR #972: 8.7 change entries | Maxime Dénès | |
| 2017-08-17 | Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵ | Maxime Dénès | |
| trailing / and \ on windows) | |||
| 2017-08-17 | Merge PR #974: Change section caption, improve some wording | Maxime Dénès | |
| 2017-08-17 | Merge PR #976: Document anonymous universes (PR #544). | Maxime Dénès | |
| 2017-08-17 | Use the wording suggested by Gaetan. | Théo Zimmermann | |
| 2017-08-17 | Addition suggested by Pierre-Marie. | Théo Zimmermann | |
| 2017-08-17 | Change 8.7~alpha to 8.7+alpha. | Maxime Dénès | |
| Only the latter is a valid git tag, and we will soon be using those to generate our version numbers. | |||
| 2017-08-17 | Make Travis generate OSX packages. | Maxime Dénès | |
| The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq | |||
| 2017-08-17 | Document anonymous universes (PR #544). | Gaëtan Gilbert | |
| 2017-08-17 | Adding documentation for Printing Focused option. | Pierre Courtieu | |
| 2017-08-16 | Additions following Hugo's suggestions. | Théo Zimmermann | |
| 2017-08-16 | mention that tactic is the identity or gives error | Paul Steckler | |
| 2017-08-16 | Improve wording. | Théo Zimmermann | |
| 2017-08-16 | Mention tclINDEPENDENTL (#349) in dev/doc/changes. | Théo Zimmermann | |
| 2017-08-16 | 8.7 CHANGES | Théo Zimmermann | |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler | |
| 2017-08-16 | Porting #856 (8.6.1 CHANGES entries) to master | Théo Zimmermann | |
| 2017-08-16 | Merge PR #957: Set detachable windows type hint to dialog. | Maxime Dénès | |
| 2017-08-16 | Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style | Maxime Dénès | |
| 2017-08-16 | Merge PR #912: Detyping functions are now operating on EConstr.t. | Maxime Dénès | |
| 2017-08-16 | Merge PR #942: solving b1859 | Maxime Dénès | |
| 2017-08-16 | Merge PR #954: Print names of all open blocks | Maxime Dénès | |
| 2017-08-16 | Merge PR #964: More portable location for the time command. | Maxime Dénès | |
| 2017-08-16 | Merge PR #951: Makefile: install-byte works even if -coqide no | Maxime Dénès | |
| 2017-08-16 | Merge PR #841: Timorous fix of bug #5598 on global existing class in sections | Maxime Dénès | |
| 2017-08-16 | Merge PR #948: [doc] Write (@nil nat) instead of (nil nat) | Maxime Dénès | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |