aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
Reviewed-by: silene
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing ↵Pierre-Marie Pédrot
time and use location in some typing error messages Reviewed-by: ppedrot
2020-10-12Merge PR #13185: Add missing ";" in Record grammarcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-12Merge PR #13156: Store the resolver of required modules as functor ↵coqbot-app[bot]
parameters in safe_env Reviewed-by: herbelin
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-12Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-12Merge PR #13175: [ci] elpi 1.11.4coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: MSoegtropIMC
2020-10-12Check types when converting irrelevant terms in old unificationGaëtan Gilbert
Fixes probably many strange issues such as the example in #13171
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
This improves the error message on the example for #13171, however we may question whether there should be an error at all.
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
Fix #13171
2020-10-12Respect Print Universes when printing primitive arraysGaëtan Gilbert
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Janno Ack-by: gares
2020-10-12Merge PR #12950: Notations: reworking the treatment of only-parsing and ↵coqbot-app[bot]
only-printing notations Reviewed-by: SkySkimmer
2020-10-12Automatically merge overlays with most recent upstream versionGaëtan Gilbert
This avoids the need to rebase the overlay when nothing has changed.
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
2020-10-11Modify Strings/String.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Strings/Ascii.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorEq.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorSpec.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/VectorDef.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Vectors/Fin.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify micromega/OrderedRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Euclid.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Div2.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify Arith/Even.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify setoid_ring/Ring.v to compile with -mangle-namesJasper Hugunin
2020-10-11Modify setoid_ring/InitialRing.v to compile with -mangle-namesJasper Hugunin
2020-10-11Similarly remove the explicit graph argument in the ~evar conversion API.Pierre-Marie Pédrot
2020-10-11Pick the universe graph out of the environment in conversion API.Pierre-Marie Pédrot
2020-10-11Remove the compare_graph field from the conversion API.Pierre-Marie Pédrot
We know statically that the first thing the conversion algorithm is going to do is to get it from the provided function, so we simply explicitly pass it around.
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
We simply use evars instance in the right order while reading back VM values.
2020-10-10Adding change log for #12950.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-08 17:40:25 +0000