aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-03Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to interpretatio...Pierre-Marie Pédrot
2018-11-03Merge PR #8844: Move abstract out of tactics.mlPierre-Marie Pédrot
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
2018-11-02Simplify use of polymorphism/program globals in attributesGaëtan Gilbert
2018-11-02rewrite: attributes handle is_univ_poly, is_program_modeGaëtan Gilbert
2018-11-02Command driven attributes.Gaëtan Gilbert
2018-11-02Move attributes out of vernacinterp to new attributes moduleGaëtan Gilbert
2018-10-31Fixes rest of #3468 (tactic-in-term was not respecting scopes).Hugo Herbelin
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-31Merge PR #8864: Avoid passing empty environmentsPierre-Marie Pédrot
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
2018-10-30Remove fully_empty_glob_sign which uses a dummy environmentMaxime Dénès
2018-10-30Distinguish globalization and pretyping error on unbound variableMaxime Dénès
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
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-19Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 02:21:42 +0000