aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-09-23Merge PR #8465: Small cleanup of summary usesPierre-Marie Pédrot
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...Enrico Tassi
2018-09-19Remove Hints.add_hints_initGaëtan Gilbert
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: simpler parsing rulesVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-14Retroknowledge.KInt31: remove the (unused) group parameterVincent Laporte
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-08-31Extraargs: avoid two token declarations to appear in all .voPierre Letouzey
2018-08-31Tacenv: minor code cleanupPierre Letouzey
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-13Less crazy implementation of the "pose" family of tactics.Pierre-Marie Pédrot
2018-07-26Merge PR #8050: Cleanup VERNAC EXTENDMaxime Dénès
2018-07-21Fixing capital letters in the "in" syntax of instantiate.Hugo Herbelin
2018-07-20Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
2018-07-12Statically typecheck the VERNAC EXTEND wrapper.Pierre-Marie Pédrot
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-10Export a function to apply toplevel tactic values in Tacinterp.Pierre-Marie Pédrot
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-05refine: obey the use_unification_heuristics flagMatthieu Sozeau
2018-07-05Merge PR #7746: Many small cleanups removing unused arguments and functionsPierre-Marie Pédrot
2018-07-03Evarutil.(e_)new_Type: remove unused env argumentGaëtan Gilbert
2018-07-03Taccoerce: remove various unused arguments.Gaëtan Gilbert
2018-07-03Pptactic: remove unused argumentsGaëtan Gilbert
2018-07-02Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:57:12 +0000