aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2016-10-25Merge remote-tracking branch 'github/pr/338' into v8.5Maxime Dénès
2016-10-25Remove warning now that info_auto is fixed.Théo Zimmermann
2016-10-25Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Maxime Dénès
2016-10-22Fixing printing of generic arguments of tag "var".Hugo Herbelin
2016-10-15Still a problem with debug auto printing.Hugo Herbelin
2016-10-15One more little bug in the output of "debug auto".Hugo Herbelin
2016-10-14Fixing printing of info_auto broken since 0091c528 (2014).Hugo Herbelin
2016-10-10Fix #4416: - Incorrect "Error: Incorrect number of goals"Arnaud Spiwack
2016-09-30Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Hugo Herbelin
2016-09-30Merge branch '4762' into v8.5Maxime Dénès
2016-09-30Fix #4762.Cyprien Mangin
2016-09-29Fix a bug in subst releaved by an OCaml warning.Maxime Dénès
2016-09-24Ensuring that the evar name is preserved by "rename" as it is alreadyHugo Herbelin
2016-09-01Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior).Hugo Herbelin
2016-08-19Remove extraneous dot in error message (bug #4832).Guillaume Melquiond
2016-08-17Fixing #5001 (metas not cleaned properly in clenv_refine_in).Hugo Herbelin
2016-07-29Fix bug #4673: regression in setoid_rewrite.Matthieu Sozeau
2016-07-29Fix #4769, univ poly and elim schemes in sectionsMatthieu Sozeau
2016-07-26Fix bug #4754, allow conversion problems to remainMatthieu Sozeau
2016-07-20Fix bug #4780: universe leak in letin_tacMatthieu Sozeau
2016-07-04Revert "Improve the interpretation scope of arguments of an ltac match."Maxime Dénès
2016-07-01Fixing use of "Declare Implicit Tactic" in refine.Hugo Herbelin
2016-07-01Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Hugo Herbelin
2016-06-14Merge branch 'bug4450' into v8.5Matthieu Sozeau
2016-06-11Fixing a try with in apply that has become too weak in 8.5.Hugo Herbelin
2016-06-09Improve the interpretation scope of arguments of an ltac match.Hugo Herbelin
2016-06-09Univs/(e)auto: fix bug #4450 polymorphic exact hintsMatthieu Sozeau
2016-05-31Revert "Rename Lexer -> CLexer."Pierre-Marie Pédrot
2016-05-29Fix bug #4746: Anomaly: Evar ?X10 was not declared.Pierre-Marie Pédrot
2016-05-26rewrite/Univs: Fix bug # 4498.Matthieu Sozeau
2016-05-23Hints/Univs: fix bug #4628 anomaliesMatthieu Sozeau
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
2016-05-03Fix bug #4707: clearbody much slower in 8.5pl1.Pierre-Marie Pédrot
2016-04-07Allow to unset the refinement mode of Instance in MLMatthieu Sozeau
2016-04-07Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-04-03Fixing the "No applicable tactic" non informative error messageHugo Herbelin
2016-03-20Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Pierre-Marie Pédrot
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-02-28Fixing bug #4596: [rewrite] broke in the past few weeks.Pierre-Marie Pédrot
2016-02-23Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Matthieu Sozeau
2016-02-19Fix regression from 8.4 in reflexivity/...Matthieu Sozeau
2016-02-17Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").Pierre-Marie Pédrot
2016-01-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-24Fixing bug #4511: evar tactic can create non-typed evars.Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2016-01-19Fix bug #4420: check_types was losing universe constraints.Matthieu Sozeau
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-11Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 23:57:09 +0000