| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-29 | Merge PR #10018: Document unshelve (#3225) | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-04-29 | Merge PR #10021: More robust timing test. | Enrico Tassi | |
| Reviewed-by: gares | |||
| 2019-04-29 | Test-suite: add a case for issue #9180 | Vincent Laporte | |
| 2019-04-29 | Revert #8187 | Vincent Laporte | |
| 2019-04-29 | Revert #9249 | Vincent Laporte | |
| 2019-04-29 | More robust timing test. | Jason Gross | |
| 2019-04-29 | Merge PR #9997: CoqIDE: fix open-file dialog and icons on macOS | Enrico Tassi | |
| Ack-by: SkySkimmer Reviewed-by: gares | |||
| 2019-04-29 | [meta] [dune] Fix discrepancies in plugin names | Emilio Jesus Gallego Arias | |
| We have some discrepancy with the package names for plugins in the META / Dune case. This PR fixes it. At some point there was a need for plugin package names having to be named as their directories. I think this is not true anymore, but taking the "dir_name == package_name" convention just in case. | |||
| 2019-04-28 | Update behavior of -emacs to support showing diffs in ProofGeneral (master ↵ | Jim Fehrle | |
| branch) Adds XML-like tags in output to mark diffs | |||
| 2019-04-29 | Document unshelve (#3225) | Paolo G. Giarrusso | |
| I believe this is the appropriate place for users to read about this, even tho `unshelve` is technically a tactical. This example was explicitly requested in #3225 and is commonly used in both Iris (and was documented in the changelog at the time). | |||
| 2019-04-28 | Merge PR #10010: [ci/gitlab] Remove after_switch message (not useful anymore). | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-04-28 | Merge PR #9605: [coq_makefile] Enforce warn_error for plugins. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares | |||
| 2019-04-28 | [test-suite] Remove a test with a Timeout that fails frequently on CI. | Théo Zimmermann | |
| 2019-04-27 | Updating CHANGES. | Hugo Herbelin | |
| 2019-04-27 | CoqIDE, cosmetic: removing obsolete comments. | Hugo Herbelin | |
| There is no more uses of "old style preferences" but the comment was still there. | |||
| 2019-04-27 | CoqiDE: Load coqide.keys after coqiderc (addressing part of #9899). | Hugo Herbelin | |
| This avoids the modifiers keys to overwrite changes made in coqide.keys. | |||
| 2019-04-27 | Minor doc improvement. | Théo Zimmermann | |
| 2019-04-27 | [refman] Fix typo. | Théo Zimmermann | |
| Noticed by Maxime Dénès. | |||
| 2019-04-27 | [ci/gitlab] Remove after_switch message (not useful anymore). | Théo Zimmermann | |
| This was put in place for @coqbot to detect runner failures, but now the strategy is different. | |||
| 2019-04-27 | Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS. | Hugo Herbelin | |
| Indeed, MacOS has a BSD uname and BSD uname does not support the -o option. Based on the following resources about uname compatility: https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux https://en.wikipedia.org/wiki/Uname | |||
| 2019-04-26 | Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974) | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-04-26 | Merge PR #9981: [dune] Build coqc.byte executable. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 Ack-by: rgrinberg | |||
| 2019-04-26 | Merge PR #9990: [opam] Use version to provide better package bounds. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-04-26 | Merge PR #10001: Add a typing colon in the output of the Search ssreflect ↵ | Enrico Tassi | |
| vernacular Reviewed-by: gares | |||
| 2019-04-26 | [opam] Use version to provide better package bounds. | Emilio Jesus Gallego Arias | |
| I copied this from Ralf Jung's submission to the Coq Package index, let's see if it works. | |||
| 2019-04-25 | [vernac] [ast] Make location info an attribute of vernaculars. | Emilio Jesus Gallego Arias | |
| This has been a mess for quite a while, we try to improve it. | |||
| 2019-04-25 | Merge PR #9999: Fix PKG in ide/.merlin.in for gtk3 | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2019-04-25 | CoqIDE: install icons on macOS | Vincent Laporte | |
| 2019-04-25 | inferCumulativity: shortcut for all-Invariant inductives | Gaëtan Gilbert | |
| 2019-04-25 | Add a typing colon in the output of the Search ssreflect vernacular | Erik Martin-Dorel | |
| See also PR math-comp/math-comp#73 | |||
| 2019-04-25 | Fix PKG in ide/.merlin.in for gtk3 | Gaëtan Gilbert | |
| 2019-04-25 | CoqIDE: fix open-file dialog on macOS | Vincent Laporte | |
| 2019-04-25 | coq_makefile: do not pass -opt/-byte to coqc (fix #9974) | Enrico Tassi | |
| 2019-04-25 | Merge Ltac2 plugin | Maxime Dénès | |
| 2019-04-25 | Prepare merge into Coq | Maxime Dénès | |
| 2019-04-24 | Merge PR #9988: [refman] Properly define token regexp. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-04-24 | Merge PR #9989: [refman] Fix a quoting problem. | Clément Pit-Claudel | |
| Reviewed-by: cpitclaudel | |||
| 2019-04-24 | [refman] Fix a quoting problem. | Théo Zimmermann | |
| 2019-04-24 | [refman] Properly define token regexp. | Théo Zimmermann | |
| 2019-04-24 | [coq_makefile] Enforce warn_error for plugins. | Emilio Jesus Gallego Arias | |
| The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974 | |||
| 2019-04-24 | Fix proof bullet error helper (nosuchgoal) | Gaëtan Gilbert | |
| The [int] is incorrect for list focusing, we could work a bit harder to fix that. It's only used for pluralisation in the error message "no such goal(s)" so we could also ignore the issue. | |||
| 2019-04-24 | [proof] Fix proof bullet error helper which was implemented as a hook | Emilio Jesus Gallego Arias | |
| We add the information on the proper layer by catching the low-level exception. | |||
| 2019-04-24 | Allocate only one evar when applying a group of conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-24 | Code factorization in conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-24 | [dune] Build coqc.byte executable. | Emilio Jesus Gallego Arias | |
| This may be useful in a few cases, like testing compilation with byte-plugins; I chose to install it globally tho it is more of a developer target. | |||
| 2019-04-23 | Deprecate the *_no_check variants of conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-23 | Merge PR #9962: [native compiler] Encoding of constructors based on tags | Pierre-Marie Pédrot | |
| Ack-by: maximedenes Reviewed-by: ppedrot | |||
| 2019-04-23 | [ssr] set under's tactic argument at LEVEL 3 | Erik Martin-Dorel | |
| So if the underlying tactic "contains a ;" one should actually write: under eq_bigl => i do [rewrite andb_idl; first by move/eqP->]. | |||
| 2019-04-23 | [ssr] under: optimization of the tactic for (under eq_bigl => *) | Erik Martin-Dorel | |
| so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over." | |||
| 2019-04-23 | [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations | Erik Martin-Dorel | |
| as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |