aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
AgeCommit message (Expand)Author
2019-05-14Remove the elimrename field from Tactics.eliminator.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-04-29Exposing a change_no_check tactic.Hugo Herbelin
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
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-08-13Less crazy implementation of the "pose" family of tactics.Pierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-28Tactics.introduction: remove dangerous option ~checkEnrico Tassi
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-30Adding "epose", "eset", "eremember" which allow to set terms withHugo Herbelin
2017-04-25Make opaque optional only for tclABSTRACTJason Gross
2017-04-25Generalize cache_term_by_tactic_thenJason Gross
2017-04-25Add support for transparent abstract (no syntax)Jason Gross
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-06-18Adding an "as" clause to specialize.Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 16:49:14 +0000