aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2016-01-07Fix bug #4480: progress was not checked for setoid_rewrite.Matthieu Sozeau
2015-12-16FIx parsing of tactic "simple refine".Maxime Dénès
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Refine tactic now shelves unifiable holes.Pierre-Marie Pédrot
2015-12-15Changing the order of the goals generated by unshelve.Pierre-Marie Pédrot
2015-12-11Add tactic native_cast_no_check, analog to vm_cast_no_check.Maxime Dénès
2015-12-10Fixing a pat%constr bug. Thanks to Enrico for reporting.Hugo Herbelin
2015-12-10Silently ignore requests to _not_ clear something when that something cannot ...Guillaume Melquiond
2015-12-09Fixing parsing of the unshelve tactical.Pierre-Marie Pédrot
2015-12-09Adding an unshelve tactical.Pierre-Marie Pédrot
2015-12-07Fix some typos.Guillaume Melquiond
2015-12-04Fix in setoid_rewrite in Type: avoid the generation of a rigid universeMatthieu Sozeau
2015-12-02Slight simplification of code for pat/constr.Hugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-11-27Fix [Polymorphic Hint Rewrite].Matthieu Sozeau
2015-11-23Fix generation of equality schemes on polymorphic equality types.Matthieu Sozeau
2015-11-19Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Pierre-Marie Pédrot
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-18Improve error message.Maxime Dénès
2015-11-17More optimizations of [Clenv.clenv_fchain].Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-13Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
2015-11-10Typo.Hugo Herbelin
2015-11-10Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Pierre-Marie Pédrot
2015-11-07Preservation of the name of evars/goals when applying pose/set/intro/clearbody.Hugo Herbelin
2015-11-05Fix bug #4273Matthieu Sozeau
2015-11-04Hint Cut documentation and cleanup of printing (was duplicated andMatthieu Sozeau
2015-11-04Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusionMatthieu Sozeau
2015-11-02Fix bug #4397: refreshing types in abstract_generalize.Matthieu Sozeau
2015-11-02Fix bug #4151: discrepancy between exact and eexact/eassumption.Matthieu Sozeau
2015-10-29Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)Guillaume Melquiond
2015-10-29Fixing another instance of bug #3267 in eauto, this time in theHugo Herbelin
2015-10-28Univs: local names handling.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:19:23 +0000