aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-14ssr: rewrite: do resolve TC once and forall at the very endEnrico Tassi
2018-11-14ssr: elim: do resolve TC once and forall at the very endEnrico Tassi
2018-11-14ssrcommon: API to call resolve_tyclasses on a termEnrico Tassi
2018-11-14ssrmatching: unify_HO does not resolve type classesEnrico Tassi
2018-11-13[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.Emilio Jesus Gallego Arias
2018-11-12Merge PR #8972: Fix #4771: Substitution of inline global reference in tactics...Pierre-Marie Pédrot
2018-11-12Merge PR #8938: [Plugins] Remove some dead codePierre-Marie Pédrot
2018-11-12Fix #4771: Substitution of inline global reference in tactics is brokenMaxime Dénès
2018-11-07[Funind plugin] Remove some dead codeVincent Laporte
2018-11-07[Firstorder plugin] Remove some dead codeVincent Laporte
2018-11-07[CC plugin] Remove dead codeVincent Laporte
2018-11-07[R syntax plugin] Remove some dead codeVincent Laporte
2018-11-07[doc] nodes in ssr are monospaceEnrico Tassi
2018-11-07multi line comments don't have a titleEnrico Tassi
2018-11-07[doc] adapt comments in plugins/ssr/*.v to coqdoc styleEnrico Tassi
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-11-06Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)Maxime Dénès
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-02Remove is_universe_polymorphism in funindGaë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-31Clarify meaning of boolean in IPatDispatchMaxime Dénès
2018-10-31[ssr] better doc for the IPatDispatch ASTEnrico Tassi
2018-10-31[ssr] use tclDISPATCH for IPatDispatch (fix #8544)Enrico Tassi
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-30Avoid passing dummy env to error printerMaxime Dénès
2018-10-30Remove one use of empty_env in ssrMaxime Dénès
2018-10-30Avoid redefining reduction functions in fun_indMaxime 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-29Merge PR #8667: [RFC] Vendoring of Camlp5Pierre-Marie Pédrot
2018-10-29Merge PR #8812: [ssreflect] Better use of CoqlibEnrico Tassi
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-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-24[ssreflect] Better use of CoqlibVincent Laporte
2018-10-19Merge PR #8758: [api] Qualify access to `Nametab`Hugo Herbelin
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-19Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:51:00 +0000