aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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-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-02{new,setoid_}ring -> ringMaxime Dénès
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
2020-09-30Fix retyping anomaly in rewriteGaëtan Gilbert
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
2020-09-29Applying ocamlformat.Hugo Herbelin
2020-09-29Almost fully moving funind to new proof engine.Hugo Herbelin
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
2020-09-18Merge PR #12610: [leminv] [declare] Use higher-level Declare API.Pierre-Marie Pédrot
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
2020-09-16More improvements in locating tactic errors.Hugo Herbelin
2020-09-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
2020-09-15[micromega] call csdpcert using path.Emilio Jesus Gallego Arias
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[ocamlformat] Update to ocamlformat 0.15.0Emilio Jesus Gallego Arias
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-06Fix printing of `change` tactic, which was printed as `change_no_check` and v...Lasse Blaauwbroek
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
2020-08-28Merge PR #12890: ring: generate fresh names for lemmascoqbot-app[bot]
2020-08-28Merge PR #11742: [numeral] [plugins] Remove Coq's `Bigint` module in favor of...coqbot-app[bot]
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-27[nsatz] num → zarithVincent Laporte
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-25omega: stop using intro_usingGaëtan Gilbert
2020-08-25funind: stop using intro_usingGaëtan Gilbert
2020-08-25ring: generate fresh names for lemmasGaëtan Gilbert
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its declar...Maxime Dénès
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:44:30 +0000