| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-24 | Add combinators to drop the bodies of local declarations. | Pierre-Marie Pédrot | |
| 2018-07-24 | Merge PR #8040: [ci] Enable native compiler in `egde:flambda` build. | Gaëtan Gilbert | |
| 2018-07-24 | [ci] Enable native compiler in `egde:flambda` build. | Emilio Jesus Gallego Arias | |
| OCaml 4.07.0 should have fixed the (memory eating bug)[https://caml.inria.fr/mantis/view.php?id=7630] | |||
| 2018-07-24 | Merge PR #6801: Highlight differences between successive proof steps (color, ↵ | Emilio Jesus Gallego Arias | |
| underline, etc.) | |||
| 2018-07-24 | Merge PR #8083: Add test for repeated section with same name | Théo Zimmermann | |
| 2018-07-24 | Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT. | Maxime Dénès | |
| 2018-07-24 | Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], ↵ | Hugo Herbelin | |
| [N], [nat] and [string] | |||
| 2018-07-23 | Make tokenize_string an optional parameter for diff methods in pp_diffs. | Jim Fehrle | |
| Remove forward reference to lexer. | |||
| 2018-07-23 | Displays the differences between successive proof steps in coqtop and CoqIDE. | Jim Fehrle | |
| Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or "-diffs on|off|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and "end.diff.*", but only on the first and last strings of the span. | |||
| 2018-07-23 | Add test for repeated section with same name | Jasper Hugunin | |
| 2018-07-23 | Make the out_channel for the log file accessible so tests can write to it ↵ | Jim Fehrle | |
| (e.g. for debugging) | |||
| 2018-07-23 | Generate more compact escape sequences by | Jim | |
| a) not explicitly setting the default value and b) not repeating attributes that are already set. Example (omitting escape character): Old: E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m New: E : [92mev[0m n (92 is bright green, the other codes set default attributes). | |||
| 2018-07-22 | Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' ↵ | Théo Zimmermann | |
| of the Reference Manual. | |||
| 2018-07-21 | Solved problems with snippets giving errors in chapter 'Detailed examples of ↵ | Zeimer | |
| tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged. | |||
| 2018-07-21 | Rewrote examples about permutations, logic and type isomorphisms: changed ↵ | Zeimer | |
| the formatting and renamed the tactics to match modern naming conventions. | |||
| 2018-07-21 | Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵ | Zeimer | |
| Manual. | |||
| 2018-07-21 | Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵ | Théo Zimmermann | |
| and 'Tactics' of the Reference Manual. | |||
| 2018-07-21 | Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual. | Théo Zimmermann | |
| 2018-07-20 | Small improvements suggested in comments to PR #8086. | Zeimer | |
| 2018-07-20 | Improved chapter 'The tactic language' of the Reference Manual. | Zeimer | |
| 2018-07-20 | Added :undocumented: and :cmd: as suggested in comments for PR #8072. | Zeimer | |
| 2018-07-20 | Fixed many spelling and grammar errors in the chapters 'Vernacular ↵ | Zeimer | |
| commands', 'Proof handling' and 'Tactics' of the Reference Manual. Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red. | |||
| 2018-07-20 | Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp. | Enrico Tassi | |
| 2018-07-20 | Merge PR #8089: Remove declare_object for SsrHave NoTCResolution. | Enrico Tassi | |
| 2018-07-20 | Merge PR #8070: Fixed some typos and grammar errors from section 'The ↵ | Théo Zimmermann | |
| language' of the Reference Manual. | |||
| 2018-07-19 | Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵ | Zeimer | |
| of the Reference Manual. | |||
| 2018-07-19 | Fixed some typos and grammar errors from section 'The language' of the ↵ | Zeimer | |
| Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes. | |||
| 2018-07-19 | Merge PR #7941: Extend QuestionMark to produce a better error message in ↵ | Pierre-Marie Pédrot | |
| case of missing record field | |||
| 2018-07-19 | Remove declare_object for SsrHave NoTCResolution. | Maxime Dénès | |
| IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality. | |||
| 2018-07-18 | Merge PR #8054: [dev] Autogenerate OCaml dev files. | Enrico Tassi | |
| 2018-07-18 | Merge PR #7897: Remove fourier plugin | Enrico Tassi | |
| 2018-07-18 | Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence` | Enrico Tassi | |
| 2018-07-18 | Merge PR #8060: Remove useless libobject in proof_using | Enrico Tassi | |
| 2018-07-17 | Merge PR #8055: Fast accumulator check in native compilation | Maxime Dénès | |
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-17 | change into QuestionMark default | Siddharth Bhat | |
| 2018-07-17 | Add overlay for Coq-Equations for QuestionMark. | Siddharth Bhat | |
| The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this. | |||
| 2018-07-17 | Change QuestionMark for better record field missing error message. | Siddharth Bhat | |
| While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields. | |||
| 2018-07-16 | Merge PR #8069: Only check overlay extensions on git-tracked files | Gaëtan Gilbert | |
| 2018-07-16 | bin,oct,hex conversions positive,Z,N,nat<->string | Jason Gross | |
| 2018-07-16 | Only check overlay extensions on git-tracked files | Jason Gross | |
| This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git. | |||
| 2018-07-16 | Merge PR #8023: Introduce a team of code owners for the CI system. | Maxime Dénès | |
| 2018-07-16 | Merge PR #8066: [ltac] Remove unused functions. | Pierre-Marie Pédrot | |
| 2018-07-14 | [build] Build Coq and plugins with `-strict-sequence` | Emilio Jesus Gallego Arias | |
| Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins. | |||
| 2018-07-14 | [ltac] Remove unused functions / constructors. | Emilio Jesus Gallego Arias | |
| Catched by compiling the ml files from ml4. | |||
| 2018-07-13 | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵ | Théo Zimmermann | |
| the Reference Manual (Introduction, Credits). | |||
| 2018-07-13 | Remove useless libobject in proof_using | Maxime Dénès | |
| 2018-07-13 | Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib. | Emilio Jesus Gallego Arias | |
| 2018-07-13 | Make -warn-error fail on warnings emitted by coqc on stdlib. | Maxime Dénès | |
| We turn all Coq warnings that are on by default into errors. | |||
| 2018-07-13 | Generate type-specific code for is_accu in native compilation of fixpoints. | Pierre-Marie Pédrot | |
| This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |