aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-26universes_of_constr: don't ignore CaseInvert universesGaëtan Gilbert
Not sure if we can get a bug from this omission.
2020-10-26Merge PR #13137: [ltac] Avoid magic numberscoqbot-app[bot]
Reviewed-by: herbelin
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: mattam82 Ack-by: pi8027 Ack-by: herbelin Ack-by: gares Ack-by: fajb Ack-by: proux01
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-24Merge PR #13263: Correct doc using :>>coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: jfehrle
2020-10-23Correct doc using :>>Gaëtan Gilbert
The cast keywords are <: and <<:, not :>/:>> :>> stopped being a keyword in #13106
2020-10-23Merge PR #13261: Fix overlay merge commandcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-23Fix overlay merge commandGaëtan Gilbert
Git wants an identity and none is setup on the CI.
2020-10-23Merge PR #13177: Automatically merge overlays with most recent upstream versioncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
Always generate prodn* files if edits succeed
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
Reviewed-by: jfehrle
2020-10-22Merge PR #13243: Fix bench variablesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-22Merge PR #13245: [default.nix] Propagate OCaml and findlib to user env.Vincent Laporte
Reviewed-by: vbgl
2020-10-22[default.nix] Propagate OCaml and findlib to user env.Théo Zimmermann
This allows native_compute to work and is the same fix that was applied to the nixpkgs repo in NixOS/nixpkgs#101058.
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under ↵Pierre-Marie Pédrot
lambda Reviewed-by: ppedrot
2020-10-22Fix bench variablesGaëtan Gilbert
2020-10-22Merge PR #13198: [coqinit] Respect order of ML includescoqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
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
This fixes a regression introduced in #11618, where I didn't realize that the order of ML includes would be important as users may want to shadow it. In general I do believe that shadowing is tricky and the build system should handle it, but for now makes sense to preserver the behavior. The fix is not very nice, but we cannot afford to tweak the API as this should be backported to 8.12.1; there is a pending PR refactoring a bit more the toplevel init that should clean this up. Fixes #12771
2020-10-21Merge PR #13222: Bench: move variables to the scriptPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #12955: Reroot primitive arrays on accesscoqbot-app[bot]
Reviewed-by: maximedenes
2020-10-20Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loopcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-20Merge PR #12648: [zify] support for int63coqbot-app[bot]
Reviewed-by: vbgl Ack-by: JasonGross Ack-by: jfehrle Ack-by: silene
2020-10-20Merge PR #13180: Respect Print Universes when printing primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
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
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-10-19Better message and avoid an infinite SPLICE loopJim Fehrle
2020-10-19Bench: move variables to the scriptGaëtan Gilbert
IMO it makes more sense this way, also it's more convenient if someone wants to run the script locally.
2020-10-19Add style for smallcaps.Théo Zimmermann
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
2020-10-19Merge PR #13208: Support "Solve Obligations of <ident>"coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-19Merge PR #13197: Require at least one reference for Typeclasses ↵coqbot-app[bot]
Opaque/Transparent Reviewed-by: SkySkimmer
2020-10-19Merge PR #13194: Add flag -open Gramlib so that merlin works in gramlib with ↵coqbot-app[bot]
make Reviewed-by: SkySkimmer
2020-10-19Merge PR #13204: Consistent indentation + a few bullets in RIneq.v.coqbot-app[bot]
Reviewed-by: silene
2020-10-19Merge PR #13151: Remove the compare_graph field from the conversion API.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-19Merge PR #13166: Fixes #13165: implicit arguments in defined fields of ↵coqbot-app[bot]
record types not taken into account Reviewed-by: SkySkimmer
2020-10-19Merge PR #13207: Use list notation in examples referenced by "nsatz" ↵coqbot-app[bot]
documentation Reviewed-by: Zimmi48
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
Reviewed-by: gares
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
Reviewed-by: ppedrot
2020-10-16Merge PR #13196: For "Typeclasses eauto", search depth should be a natural, ↵Pierre-Marie Pédrot
not an integer Reviewed-by: ppedrot
2020-10-16Overlay for elpi.Hugo Herbelin
2020-10-15Support "Solve Obligations of <ident>" optionJim Fehrle
2020-10-16Add change log for #13166.Hugo Herbelin
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
Fixes implicit arguments from the body of a defined field not taken into account. Get (a bit) more information for detection of SProp relevance in implicitly-typed defined field. (It should be done at the very end of the inference phase, though, because some evars may not yet be instantiated.)
2020-10-16Generalizing and exporting interp_assumption/interp_definition.Hugo Herbelin
This shall be for Record fields consumption.
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:42:25 +0000