aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* [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
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
| * Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
| * Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
|/
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* | Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
|/
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
* Tacticals: typo in a commentGravatar Pierre Letouzey2016-02-16
* New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
|/ /
* / Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
|/
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07