aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-09Modify ZArith/ZArith_dec.v to compile with -mangle-namesJasper Hugunin
2020-10-09Modify Bool/Sumbool.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/Zorder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify setoid_ring/Ring_polynom.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify ZArith/BinInt.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZBits.v to compile with -mangle-namesJasper Hugunin
As before, add a `bitwise as` tactic notation.
2020-10-08Modify Numbers/Integer/Abstract/ZLcm.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZGcd.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivFloor.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZDivTrunc.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZPow.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZParity.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZSgnAbs.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZMulOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-10-08Modify Numbers/Integer/Abstract/ZAdd.v to compile with -mangle-namesJasper Hugunin
All that really needed to be done was add an explicit intro before nzinduct, but all the issues in this file could be fixed by moving n m p before the colon, and I couldn't stop my self.
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a ↵coqbot-app[bot]
specific format. Reviewed-by: ejgallego
2020-10-08Merge PR #13159: update for Iris build system changescoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-08update for Iris build system changesRalf Jung
2020-10-08Merge PR #13128: Define a new type instance_flag instead of using [unit option]Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Merge PR #13152: Algorithmically faster implementation of ↵coqbot-app[bot]
Evarconv.apply_on_subterm Reviewed-by: mattam82
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Merge PR #13119: Fix retyping anomaly in rewritePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-07Explicitly pass around a state in Evarconv.second_order_matching.Pierre-Marie Pédrot
I know higher-order mutable state shared across call sites is a staple of Matthieu's style, but it is a footgun begging to be abused.
2020-10-07Algorithmically faster implementation of Evarconv.apply_on_subterm.Pierre-Marie Pédrot
Instead of repeatedly checking for evars to appear in a term, we perform the search in one single pass. This slowdown was observed in fiat-crypto. This is still a naive algorithm though, since we recompute the set of evars for each subterm. This is thus quadratic.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:58:25 +0000