| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-26 | [sphinx] Do name cleanup in handle_signature | Clément Pit-Claudel | |
| 2018-07-25 | [sphinx] Add a way of skipping names in the indexes. | Théo Zimmermann | |
| 2018-07-25 | Merge PR #8139: Replace all the CoInductives with Variants in the SSR plugin | Enrico Tassi | |
| 2018-07-25 | Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2) | Hugo Herbelin | |
| 2018-07-25 | Replace all the CoInductives with Variants in the SSR plugin | Kazuhiko Sakaguchi | |
| 2018-07-24 | Merge PR #7908: Projections use index representation | Pierre-Marie Pédrot | |
| 2018-07-24 | Merge PR #8040: [ci] Enable native compiler in `egde:flambda` build. | Gaëtan Gilbert | |
| 2018-07-24 | Add simple test cases for vm and native on primitive projections. | Gaëtan Gilbert | |
| 2018-07-24 | VM: don't duplicate projection narg information in lproj/kproj | Gaëtan Gilbert | |
| 2018-07-24 | Add overlay for Equations. | Gaëtan Gilbert | |
| 2018-07-24 | Fix #7329: coqchk Include with primitive projections | Gaëtan Gilbert | |
| 2018-07-24 | Projections use index representation | Gaëtan Gilbert | |
| The upper layers still need a mapping constant -> projection, which is provided by Recordops. | |||
| 2018-07-24 | Remove useless is_projection in tacred | Gaëtan Gilbert | |
| 2018-07-24 | Move Heads to pretyping (is_projection will move to Recordops) | 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |