aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...Emilio Jesus Gallego Arias
2020-05-15Merge PR #11979: Add a rudimentary script to generate release changelog.Emilio Jesus Gallego Arias
2020-05-15Clarify release-process.mdEnrico Tassi
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
2020-05-15Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.Emilio Jesus Gallego Arias
2020-05-15Fix typo.Théo Zimmermann
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-15Merge PR #12032: [win] Elpi, Coq-Elpi and HBMichael Soegtrop
2020-05-15[interp] Register printers for InternalizationError instead of ad-hoc hanlding.Emilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Add advisories on OCaml setup to INSTALL.md.Théo Zimmermann
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
2020-05-14Merge PR #12327: Add a changelog for 8.11.2.Théo Zimmermann
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Merge PR #12312: Clarify the documentation for merging PRs with overlaysThéo Zimmermann
2020-05-14Fix title level and a build failure.Théo Zimmermann
2020-05-14Fix conflicts with latest master.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-14Tweak the error message of reference internalization.Pierre-Marie Pédrot
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Added change log.Hugo Herbelin
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Preserve Implicit arguments file.Théo Zimmermann
2020-05-14Remove Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Merge doc on Canonical structures from two origins.Théo Zimmermann
2020-05-14Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.Gaëtan Gilbert
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Merge PR #12320: [ci] [sf] Fix SF build.Gaëtan Gilbert
2020-05-14Add Canonical structure declarations to Canonical structures file.Théo Zimmermann
2020-05-14Extract Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Split Gallina extensions into multiple files.Théo Zimmermann
2020-05-14Split Gallina into multiple files.Théo Zimmermann
2020-05-14Split parts of CIC into multiple files.Théo Zimmermann
2020-05-14Create new file on Functions and Assumptions.Théo Zimmermann
2020-05-14Extract functions and assumptions.Théo Zimmermann
2020-05-14Merge definitions and type casts in same file.Théo Zimmermann
2020-05-14Create new file on Definitions.Théo Zimmermann
2020-05-14Extract Definitions from Gallina.Théo Zimmermann
2020-05-14Add type casts to new Definitions file.Théo Zimmermann