aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-10-09Update pretyping/detyping.mlEnrico Tassi
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-10-09Merge PR #13143: Drop misleading argument of Pp.h boxcoqbot-app[bot]
2020-10-09improve commentEnrico Tassi
2020-10-09[bench] Dump the vo size difference.Pierre-Marie Pédrot
2020-10-09overlay for minim-prop-tosetGaëtan Gilbert
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
2020-10-09Store the resolver of required modules as functor parameters in safe_env.Pierre-Marie Pédrot
2020-10-09[printing] make detyping resilient to "let x : _ := t in"Enrico Tassi
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-08Add overlays for Coq-Equations, aac-tactics.Hugo Herbelin
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-10-08Add a check of empty list of arguments in xmlprotocol where relevant.Hugo Herbelin
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-08Check complexity of primitive arrays.Guillaume Melquiond
2020-10-08Remove occurrences of Parray.reroot.Guillaume Melquiond
2020-10-08Reroot primitive arrays on access (fix #12947).Guillaume Melquiond
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-06Fixing redundant outputs when printing goals, especially in non-"pr_first" mode.Hugo Herbelin
2020-10-06Documenting option Set Printing Goal Name.Hugo Herbelin
2020-10-06Merge PR #13141: Document the removal of forward class hints.coqbot-app[bot]
2020-10-06Use OCaml floating-point operations on 64 bits archPierre Roux
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-10-06Remove unused is_class info from cl_contextGaëtan Gilbert
2020-10-06Implicit_quantifiers don't use precomputed is_class dataGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 01:06:47 +0000