aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\
* | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| * Show unused-intro-pattern warning.Gravatar Théo Zimmermann2017-03-14
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
| * \ Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \
| | * | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| * | | More precise refine compatibilityGravatar Matthieu Sozeau2016-11-05
| * | | Fix #3441 Use pf_get_type_of to avoid blowupGravatar Matthieu Sozeau2016-11-04
| * | | Fix refine in compatibility modeGravatar Matthieu Sozeau2016-11-04
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | |
| | | * Documenting changes in typeclassesGravatar Matthieu Sozeau2016-10-29
| | |/ | |/|
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\ \ | | |/ | |/|
| | * Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Gravatar Maxime Dénès2016-10-25
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| |
| * | Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Gravatar Pierre-Marie Pédrot2016-10-07
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
| |\ \
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| | |
| * | | Micro refactoring: use exact_no_check.Gravatar Théo Zimmermann2016-10-01
| * | | Fix bug #5045: [generalize] creates ill-typed terms in 8.6.Gravatar Pierre-Marie Pédrot2016-09-30
| * | | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.Gravatar Pierre-Marie Pédrot2016-09-30
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-27
| |\ \ \ | | | |/ | | |/|
| * | | Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
| | * | Ensuring that the evar name is preserved by "rename" as it is alreadyGravatar Hugo Herbelin2016-09-24
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| | |
* | | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | | | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* | | | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
| * | | Typo.Gravatar Hugo Herbelin2016-09-15
| | | * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| | |/ | |/|
* | | Removing the last uses of Pptactic in the lower layers.Gravatar Pierre-Marie Pédrot2016-09-09
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\ \ \ \ | | |/ / | |/| |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
| |\ \ \ | | | |/ | | |/|
| | * | Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior).Gravatar Hugo Herbelin2016-09-01
| * | | Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internalGravatar Hugo Herbelin2016-09-01
* | | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
|/ / /
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\| |
* | | More standard naming for the Imparg.with_implicits function.Gravatar Pierre-Marie Pédrot2016-08-20
* | | Fix performance bug: do not compute implicits of abstracted lemmas.Gravatar Pierre-Marie Pédrot2016-08-19
| | * 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
| |/ |/|
| * Fixing #5001 (metas not cleaned properly in clenv_refine_in).Gravatar Hugo Herbelin2016-08-17
| * Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 20:43:20 +0000