aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-10-12Lowercase variables in git_downloadGaëtan Gilbert
2020-10-12elpi 1.11.4Enrico Tassi
2020-10-11Modify ZArith/Znumtheory.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zdiv.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zcomplements.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyInst.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZifyClasses.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Ztac.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/ZCoeff.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zpow_def.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Wf_Z.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Zabs.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify ZArith/Znat.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/RingMicromega.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Tauto.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/Refl.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/EnvRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify NArith/Ndigits.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 00:00:58 +0000