aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
AgeCommit message (Expand)Author
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
2016-06-18A cleaning phase around delayed induction arg + exporting force_induction_arg.Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-05-17Removing the old refine tactic from the Tactics module.Pierre-Marie Pédrot
2016-05-17Put the "move" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "change" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "specialize_eq" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize dependent" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "*_cast_no_check" tactics in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "exact_constr" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-02-15Code factorization of tactic "unfold_body".Pierre-Marie Pédrot
2016-02-15More conversion functions in the new tactic API.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-14Moving is_quantified_hypothesis to new proof engine.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 16:26:12 +0000