aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-10-26Yet another normal / neutral bug in primitive conversion.Pierre-Marie Pédrot
2020-10-26Fix bug in conversion of primitive values.Pierre-Marie Pédrot
2020-10-26Merge PR #13257: adjust Search deprecation warningcoqbot-app[bot]
2020-10-26Merge PR #13223: [declare] Remove recursive declaration from non-recursive fu...coqbot-app[bot]
2020-10-26adjust Search deprecation warningRalf Jung
2020-10-26Merge PR #13137: [ltac] Avoid magic numberscoqbot-app[bot]
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-24Merge PR #13263: Correct doc using :>>coqbot-app[bot]
2020-10-23Correct doc using :>>Gaëtan Gilbert
2020-10-23Merge PR #13261: Fix overlay merge commandcoqbot-app[bot]
2020-10-23[declare] Remove recursive declaration from non-recursive functionsEmilio Jesus Gallego Arias
2020-10-23Fix overlay merge commandGaëtan Gilbert
2020-10-23Merge PR #13177: Automatically merge overlays with most recent upstream versioncoqbot-app[bot]
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
2020-10-22Merge PR #13243: Fix bench variablesPierre-Marie Pédrot
2020-10-22Merge PR #13245: [default.nix] Propagate OCaml and findlib to user env.Vincent Laporte
2020-10-22[default.nix] Propagate OCaml and findlib to user env.Théo Zimmermann
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under l...Pierre-Marie Pédrot
2020-10-22Fix bench variablesGaëtan Gilbert
2020-10-22Merge PR #13198: [coqinit] Respect order of ML includescoqbot-app[bot]
2020-10-21[coqinit] Cosmetics on long list append.Emilio Jesus Gallego Arias
2020-10-21[coqinit] Respect order of ML includesEmilio Jesus Gallego Arias
2020-10-21Merge PR #13222: Bench: move variables to the scriptPierre-Marie Pédrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
2020-10-20Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loopcoqbot-app[bot]
2020-10-20Merge PR #12648: [zify] support for int63coqbot-app[bot]
2020-10-20Merge PR #13180: Respect Print Universes when printing primitive arrayscoqbot-app[bot]
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-19Better message and avoid an infinite SPLICE loopJim Fehrle
2020-10-19Bench: move variables to the scriptGaëtan Gilbert
2020-10-19Add style for smallcaps.Théo Zimmermann
2020-10-19Merge PR #13208: Support "Solve Obligations of <ident>"coqbot-app[bot]
2020-10-19Merge PR #13197: Require at least one reference for Typeclasses Opaque/Transp...coqbot-app[bot]
2020-10-19Merge PR #13194: Add flag -open Gramlib so that merlin works in gramlib with ...coqbot-app[bot]
2020-10-19Merge PR #13204: Consistent indentation + a few bullets in RIneq.v.coqbot-app[bot]
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record...coqbot-app[bot]
2020-10-19Merge PR #13207: Use list notation in examples referenced by "nsatz" document...coqbot-app[bot]
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
2020-10-16Use list notation in nsatz examples referenced in the docJim Fehrle
2020-10-16Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>"Pierre-Marie Pédrot
2020-10-16Merge PR #13196: For "Typeclasses eauto", search depth should be a natural, n...Pierre-Marie Pédrot
2020-10-16Overlay for elpi.Hugo Herbelin
2020-10-15Support "Solve Obligations of <ident>" optionJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-08 17:59:25 +0000