aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\ \
| * | Do not normalize evars in Eauto.e_give_exact.Gravatar Pierre-Marie Pédrot2016-09-04
* | | 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
| * | | Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-08-30
* | | | 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: removing calls of the "Context.Named.Declaration.get_value" functionGravatar 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
* | | Moving Taccoerce to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-08-19
| * | Remove extraneous dot in error message (bug #4832).Gravatar Guillaume Melquiond2016-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
* | Fixing #3070 ("subst" taking properly into account chains of dependencies).Gravatar Hugo Herbelin2016-08-17
| * Fix bug #4673: regression in setoid_rewrite.Gravatar Matthieu Sozeau2016-07-29
* | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\|
| * Fix #4769, univ poly and elim schemes in sectionsGravatar Matthieu Sozeau2016-07-29
| * Fix bug #4754, allow conversion problems to remainGravatar Matthieu Sozeau2016-07-26
| * Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
* | Fix bug #4780: universe leak in letin_tacGravatar Matthieu Sozeau2016-07-20
* | Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* | primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
| * Revert "Improve the interpretation scope of arguments of an ltac match."Gravatar Maxime Dénès2016-07-04
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* | Make semantics of whd_zeta consistent with other whd_* functions.Gravatar Maxime Dénès2016-07-01
| * Fixing use of "Declare Implicit Tactic" in refine.Gravatar Hugo Herbelin2016-07-01
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| * Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Gravatar Hugo Herbelin2016-07-01
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
* | Typeclasses: fix treatment of exceptions in compatGravatar Matthieu Sozeau2016-06-27
* | Typeclasses: mark unresolvable goals in new implementationGravatar Matthieu Sozeau2016-06-27
* | We want tclORELSE to catch exceptions on backtrackingsGravatar Matthieu Sozeau2016-06-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optmimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 23:49:52 +0000