aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-26Preserving goal name in revert/bring_hyps.Hugo Herbelin
2015-10-24Fixing a loop in checking hints with holes.Hugo Herbelin
2015-10-24Backtracking on interpreting toplevel calls to exact in scope determinedHugo Herbelin
2015-10-19Categorizing debug messages as such + NonLogical uses loggers.Pierre Courtieu
2015-10-19Turning anomaly into error for #4372 (weakness of inversion in theHugo Herbelin
2015-10-16Generalize fix for auto from PMP to eauto and typeclasses eauto.Matthieu Sozeau
2015-10-16Merge hint lists instead of appending them. (Fix bug #3199)Guillaume Melquiond
2015-10-14Fixing perfomance issue of auto hints induced by universes.Pierre-Marie Pédrot
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-10-13Fix some typos.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 10:40:05 +0000