| Age | Commit message (Expand) | Author |
|---|
| 2018-07-26 | Expose the diff printing option as an UI entry in CoqIDE. | Pierre-Marie Pédrot |
| 2018-07-26 | Do not set diff printing on by default in CoqIDE. | Pierre-Marie Pédrot |
| 2018-07-26 | Merge PR #7786: In "redundant clause" pattern-matching error, show also the p... | Pierre-Marie Pédrot |
| 2018-07-26 | Merge PR #8084: Properly disable native compilation when -native-compiler is ... | Maxime Dénès |
| 2018-07-26 | Merge PR #7274: Avoiding introducing dependency on the indices of a term whic... | Pierre-Marie Pédrot |
| 2018-07-26 | Merge PR #8150: Fix static declaration of plugins in coqpp. | Emilio Jesus Gallego Arias |
| 2018-07-25 | Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ... | Pierre-Marie Pédrot |
| 2018-07-25 | Merge PR #8133: Fixes #8126: issue with notations and nested applications | Emilio Jesus Gallego Arias |
| 2018-07-25 | Merge PR #734: [travis] Also run coqchk on HoTT | Emilio Jesus Gallego Arias |
| 2018-07-25 | In "redundant clause" pattern-matching error, show also the pattern (#7777). | Hugo Herbelin |
| 2018-07-25 | Optimized dependencies for pattern-matching on only trivial patterns. | Hugo Herbelin |
| 2018-07-25 | Fix static declaration of plugins in coqpp. | Pierre-Marie Pédrot |
| 2018-07-25 | Add overlay for Equations | Gaëtan Gilbert |
| 2018-07-25 | Remove himsg.pr_puniverses, use @{} for universe printing in errors | Maxime Dénès |
| 2018-07-25 | Merge PR #7889: Cleanup reduction effects: they only work on constants. | Pierre-Marie Pédrot |
| 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 | [travis] Also run coqchk on HoTT | Jason Gross |
| 2018-07-24 | Merge PR #7908: Projections use index representation | Pierre-Marie Pédrot |
| 2018-07-24 | Properly disable native compilation when -native-compiler is unset. | 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 |
| 2018-07-24 | Fixes #8126 (issue with notations and nested applications). | Hugo Herbelin |
| 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 |
| 2018-07-24 | Merge PR #6801: Highlight differences between successive proof steps (color, ... | Emilio Jesus Gallego Arias |
| 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 |
| 2018-07-23 | Make tokenize_string an optional parameter for diff methods in pp_diffs. | Jim Fehrle |
| 2018-07-23 | Displays the differences between successive proof steps in coqtop and CoqIDE. | Jim Fehrle |
| 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 (e.... | Jim Fehrle |
| 2018-07-23 | Generate more compact escape sequences by | Jim |
| 2018-07-22 | Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' o... | Théo Zimmermann |
| 2018-07-21 | Solved problems with snippets giving errors in chapter 'Detailed examples of ... | Zeimer |
| 2018-07-21 | Rewrote examples about permutations, logic and type isomorphisms: changed the... | Zeimer |
| 2018-07-21 | Improvements for the chapter 'Detailed examples of tactics' of the Reference ... | Zeimer |
| 2018-07-21 | Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' an... | Théo Zimmermann |
| 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 commands',... | Zeimer |
