aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Still a problem with debug auto printing.Gravatar Hugo Herbelin2016-10-15
| * One more little bug in the output of "debug auto".Gravatar Hugo Herbelin2016-10-15
* | Fix bug #5139: Anomalies should not be caught by || / try.Gravatar Pierre-Marie Pédrot2016-10-14
| * Fixing printing of info_auto broken since 0091c528 (2014).Gravatar Hugo Herbelin2016-10-14
* | Fixing English typography for colon.Gravatar Hugo Herbelin2016-10-14
* | Using "simple apply" and "simple eapply" in the trace of auto.Gravatar Hugo Herbelin2016-10-14
* | Fix bug #4958: [debug auto] should specify hint databases.Gravatar Pierre-Marie Pédrot2016-10-12
| * Fix #4416: - Incorrect "Error: Incorrect number of goals"Gravatar Arnaud Spiwack2016-10-10
* | Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Gravatar Pierre-Marie Pédrot2016-10-07
* | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
* | Merge remote-tracking branch 'github/pr/263' into v8.6Gravatar Maxime Dénès2016-10-03
|\ \
* | | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-02
|\ \ \ | | |/ | |/|
* | | Micro refactoring: use exact_no_check.Gravatar Théo Zimmermann2016-10-01
| * | Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Gravatar Hugo Herbelin2016-09-30
* | | 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.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\| |
| * | Merge branch '4762' into v8.5Gravatar Maxime Dénès2016-09-30
| |\ \
| | * | Fix #4762.Gravatar Cyprien Mangin2016-09-30
| * | | Fix a bug in subst releaved by an OCaml warning.Gravatar Maxime Dénès2016-09-29
| |/ /
* | | 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
* | | Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* | | Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* | | Typo.Gravatar Hugo Herbelin2016-09-15
| | * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| |/ |/|
* | Do not normalize evars in Eauto.e_give_exact.Gravatar Pierre-Marie Pédrot2016-09-04
* | 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
* | 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
| * 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