aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mli
Commit message (Expand)AuthorAge
* Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Tactics.introduction: remove dangerous option ~checkGravatar Enrico Tassi2018-05-28
* [tactics] Remove anonymous fix/cofix form.Gravatar Emilio Jesus Gallego Arias2018-05-24
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
* | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\
* | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
* Make opaque optional only for tclABSTRACTGravatar Jason Gross2017-04-25
* Generalize cache_term_by_tactic_thenGravatar Jason Gross2017-04-25
* Add support for transparent abstract (no syntax)Gravatar Jason Gross2017-04-25
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* Adding an "as" clause to specialize.Gravatar Hugo Herbelin2016-06-18
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* A cleaning phase around delayed induction arg + exporting force_induction_arg.Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "move" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-17
* Put the "change" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize dependent" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "*_cast_no_check" tactics in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 23:57:03 +0000