aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2019-05-24Fixing typosJPR
2019-05-23Fixing typos - Part 3JPR
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
2019-05-14Remove the sidecond_first flag of apply-related tactics.Pierre-Marie Pédrot
2019-05-14Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
2019-05-14Code factorization in elim tactics.Pierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
2019-05-11Actually use the conversion locality flag.Pierre-Marie Pédrot
2019-05-11Introducing a local flag to hypothesis conversion function.Pierre-Marie Pédrot
2019-05-11Abstract the Tactic.e_change_hyps function over the reduction function.Pierre-Marie Pédrot
2019-05-10Take advantage of the ordering / conversion check split.Pierre-Marie Pédrot
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
2019-05-10Logic.convert_hyp now takes an environment as an argument.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-05Merge PR #10059: Fixing bugs introduced in change_no_checkPierre-Marie Pédrot
2019-05-04Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...Pierre-Marie Pédrot
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
2019-05-03Fix #9994: `revert dependent` is extremely slow.Pierre-Marie Pédrot
2019-05-02Remove outdated commentMaxime Dénès
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
2019-05-02Use GlobRef.Map.t in hint databasesMaxime Dénès
2019-05-02Document typeclasses_eautoMaxime Dénès
2019-04-29Exposing a change_no_check tactic.Hugo Herbelin
2019-04-24Allocate only one evar when applying a group of conversion tactics.Pierre-Marie Pédrot
2019-04-24Code factorization in conversion tactics.Pierre-Marie Pédrot
2019-04-23Deprecate the *_no_check variants of conversion tactics.Pierre-Marie Pédrot
2019-04-20Merge PR #9836: [schemes] Don't re-declare scheme side-effects that are alrea...Enrico Tassi
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-04-02Merge PR #9659: Fix #9652: rewrite fails to detect lack of progressEmilio Jesus Gallego Arias
2019-03-31Merge PR #9841: Remove some [let foo = foo] in eqschemesPierre-Marie Pédrot
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[tactic] Adapt tactic layer to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27Remove some [let foo = foo] in eqschemesGaëtan Gilbert
2019-03-26[kernel] Don't re-declare scheme side-effects that are already there.Emilio Jesus Gallego Arias
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:55 +0000