aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-07-25Fix static declaration of plugins in coqpp.Pierre-Marie Pédrot
2018-07-25Doc: preliminary work before #7291 which add an "Unable to unify" message.Hugo Herbelin
2018-07-25[ssr] assertion -> error message (Fix #8134)Enrico Tassi
2018-07-25Add overlay for EquationsGaëtan Gilbert
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
2018-07-25Merge PR #7889: Cleanup reduction effects: they only work on constants.Pierre-Marie Pédrot
2018-07-25Merge PR #8139: Replace all the CoInductives with Variants in the SSR pluginEnrico Tassi
2018-07-25Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2)Hugo Herbelin
2018-07-25Replace all the CoInductives with Variants in the SSR pluginKazuhiko Sakaguchi
2018-07-24[travis] Also run coqchk on HoTTJason Gross
2018-07-24Merge PR #7908: Projections use index representationPierre-Marie Pédrot
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Add combinators to drop the bodies of local declarations.Pierre-Marie Pédrot
2018-07-24Properly disable native compilation when -native-compiler is unset.Pierre-Marie Pédrot
2018-07-24Merge PR #8040: [ci] Enable native compiler in `egde:flambda` build.Gaëtan Gilbert
2018-07-24Add simple test cases for vm and native on primitive projections.Gaëtan Gilbert
2018-07-24VM: don't duplicate projection narg information in lproj/kprojGaëtan Gilbert
2018-07-24Add overlay for Equations.Gaëtan Gilbert
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-24Fixes #8126 (issue with notations and nested applications).Hugo Herbelin
2018-07-24Remove useless is_projection in tacredGaëtan Gilbert
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert
2018-07-24Update the documentation w.r.t. the new error raised by unify.Pierre-Marie Pédrot
2018-07-24[ci] Enable native compiler in `egde:flambda` build.Emilio Jesus Gallego Arias
2018-07-24Merge PR #6801: Highlight differences between successive proof steps (color, ...Emilio Jesus Gallego Arias
2018-07-24Merge PR #8083: Add test for repeated section with same nameThéo Zimmermann
2018-07-24Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT.Maxime Dénès
2018-07-24Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], [...Hugo Herbelin
2018-07-23Make tokenize_string an optional parameter for diff methods in pp_diffs.Jim Fehrle
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-23Make the out_channel for the log file accessible so tests can write to it (e....Jim Fehrle
2018-07-23Generate more compact escape sequences byJim
2018-07-23Adding environment-manipulating functions.Pierre-Marie Pédrot
2018-07-23Fix deprecated warnings from Pcoq.Pierre-Marie Pédrot
2018-07-23Merge remote-tracking branch 'origin/pr/54'Pierre-Marie Pédrot
2018-07-22Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' o...Théo Zimmermann
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ...Zeimer
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed the...Zeimer
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ...Zeimer
2018-07-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' an...Théo Zimmermann
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
2018-07-21[doc] Fix grammar of goal selectors.Théo Zimmermann
2018-07-21A few Sphinx fixes in the Ltac chapter.Théo Zimmermann
2018-07-21Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.Théo Zimmermann
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 05:56:01 +0000