aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-19Adding change log for #13092.Hugo Herbelin
2020-10-19Addressing parsing part #13078.Hugo Herbelin
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
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-14[build] [native] Don't assume installed native libraries are in custom output...Emilio Jesus Gallego Arias
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
2020-10-14Fix anomaly when importing a functorGaë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]
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-12Merge PR #13156: Store the resolver of required modules as functor parameters...coqbot-app[bot]
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
2020-10-12Merge PR #13175: [ci] elpi 1.11.4coqbot-app[bot]
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
2020-10-12Respect Print Universes when printing primitive arraysGaëtan Gilbert
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-12Merge PR #12950: Notations: reworking the treatment of only-parsing and only-...coqbot-app[bot]
2020-10-12Automatically merge overlays with most recent upstream versionGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 20:16:00 +0000