aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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-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
2020-10-16Add change log for #13166.Hugo Herbelin
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-16Generalizing and exporting interp_assumption/interp_definition.Hugo Herbelin
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
2020-10-15Consistent indentation + a few bullets in RIneq.v.Hugo Herbelin
2020-10-15Report a useful error for dependent destructionTej Chajed
2020-10-15Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hypPierre-Marie Pédrot
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
2020-10-15Merge PR #13144: Closes #13142: more standardized pretty-printing of Coq recordscoqbot-app[bot]
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
2020-10-15Require at least one reference for Typeclasses Opaque/TransparentJim Fehrle
2020-10-14For "Typeclasses eauto", search depth should be a natural, not anJim Fehrle
2020-10-14Add support for "typeclasses eauto bfs <int_or_var_opt>Jim Fehrle
2020-10-14Add flag -open Gramlib so that merlin works in gramlib with make.Hugo Herbelin
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-14Merge PR #13147: Use OCaml floating-point operations on 64 bits archcoqbot-app[bot]
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing tim...Pierre-Marie Pédrot
2020-10-12Merge PR #13185: Add missing ";" in Record grammarcoqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 20:06:51 +0000