aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Gravatar Maxime Dénès2016-10-25
* Fixing printing of generic arguments of tag "var".Gravatar Hugo Herbelin2016-10-22
* 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
* Fixing printing of info_auto broken since 0091c528 (2014).Gravatar Hugo Herbelin2016-10-14
* Fix #4416: - Incorrect "Error: Incorrect number of goals"Gravatar Arnaud Spiwack2016-10-10
* Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Gravatar Hugo Herbelin2016-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
|/
* Ensuring that the evar name is preserved by "rename" as it is alreadyGravatar Hugo Herbelin2016-09-24
* Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior).Gravatar Hugo Herbelin2016-09-01
* 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
* Fix bug #4673: regression in setoid_rewrite.Gravatar 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
* Revert "Improve the interpretation scope of arguments of an ltac match."Gravatar Maxime Dénès2016-07-04
* Fixing use of "Declare Implicit Tactic" in refine.Gravatar Hugo Herbelin2016-07-01
* Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Gravatar Hugo Herbelin2016-07-01
* Merge branch 'bug4450' into v8.5Gravatar Matthieu Sozeau2016-06-14
|\
* | Fixing a try with in apply that has become too weak in 8.5.Gravatar Hugo Herbelin2016-06-11
* | Improve the interpretation scope of arguments of an ltac match.Gravatar Hugo Herbelin2016-06-09
| * Univs/(e)auto: fix bug #4450 polymorphic exact hintsGravatar Matthieu Sozeau2016-06-09
|/
* Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* Fix bug #4746: Anomaly: Evar ?X10 was not declared.Gravatar Pierre-Marie Pédrot2016-05-29
* rewrite/Univs: Fix bug # 4498.Gravatar Matthieu Sozeau2016-05-26
* Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
* Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
* Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
* Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
* Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
* Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Gravatar Pierre-Marie Pédrot2016-03-20
* Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* Fixing bug #4596: [rewrite] broke in the past few weeks.Gravatar Pierre-Marie Pédrot2016-02-28
* Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Gravatar Matthieu Sozeau2016-02-23
* Fix regression from 8.4 in reflexivity/...Gravatar Matthieu Sozeau2016-02-19
* Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Gravatar Pierre-Marie Pédrot2016-02-17
* Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
* Fixing bug #4511: evar tactic can create non-typed evars.Gravatar Pierre-Marie Pédrot2016-01-24
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
* Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Gravatar Matthieu Sozeau2016-01-11
* Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
* FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 00:50:23 +0000