aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
AgeCommit message (Expand)Author
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
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-30Moving apply_type to new proof engine.Hugo Herbelin
2015-12-25Moving specialize to Proofview.tactic.Hugo Herbelin
2015-12-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-05Removing redundant versions of generalize.Hugo Herbelin
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-10-29Monotonizing Tactics.change_arg.Pierre-Marie Pédrot
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:06:41 +0000