aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a speci...coqbot-app[bot]
2020-10-08Merge PR #13159: update for Iris build system changescoqbot-app[bot]
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
2020-10-07Merge PR #13152: Algorithmically faster implementation of Evarconv.apply_on_s...coqbot-app[bot]
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
2020-10-07Merge PR #13119: Fix retyping anomaly in rewritePierre-Marie Pédrot
2020-10-07Explicitly pass around a state in Evarconv.second_order_matching.Pierre-Marie Pédrot
2020-10-07Algorithmically faster implementation of Evarconv.apply_on_subterm.Pierre-Marie Pédrot
2020-10-06Merge PR #13141: Document the removal of forward class hints.coqbot-app[bot]
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-03Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook.coqbot-app[bot]
2020-10-02Merge PR #13125: More details in the documentation of native arrayscoqbot-app[bot]
2020-10-02More details in the documentation of native arraysVincent Semeria
2020-10-02Merge PR #13054: {new,setoid_}ring -> ringcoqbot-app[bot]
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
2020-10-01Merge PR #13116: interp_context_evars: removed unused [shift] argumentcoqbot-app[bot]
2020-10-01Merge PR #13123: Fix combining uniform parameters and mutual inductives.coqbot-app[bot]
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:26:27 +0000