aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-10-16Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>"Pierre-Marie Pédrot
2020-10-16Merge PR #13196: For "Typeclasses eauto", search depth should be a natural, n...Pierre-Marie Pédrot
2020-10-14For "Typeclasses eauto", search depth should be a natural, not anJim Fehrle
2020-10-14Add support for "typeclasses eauto bfs <int_or_var_opt>Jim Fehrle
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is de...Hugo Herbelin
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 10:35:08 +0000