aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in 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
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| * Fixing a subtle bug in tclWITHHOLES.Gravatar Hugo Herbelin2017-05-28
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [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
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
* | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Proofview.Goal primitive now return EConstrs.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
* | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * | Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
|/ /
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Fix bug #5139: Anomalies should not be caught by || / try.Gravatar Pierre-Marie Pédrot2016-10-14
* | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* 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
* | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \