aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
AgeCommit message (Expand)Author
2016-06-02Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...Hugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Remove some unused functions.Guillaume Melquiond
2015-11-18Inlining the only use of Clenv.connect_clenv.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-19Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-16Generalize fix for auto from PMP to eauto and typeclasses eauto.Matthieu Sozeau
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-10-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-06Fix bug #4354: interpret hints in the right env and sigma.Matthieu Sozeau
2015-07-27Add an Iterative Deepening search strategy to typeclass resolution.Matthieu Sozeau
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29class_tactics: make interruptibleEnrico Tassi
2015-06-29class_tactics: remove catch-all, use Errors.noncriticalEnrico Tassi
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-11Rationalizing a bit the interface of Hints.Pierre-Marie Pédrot
2015-04-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-09Fix caching of local hintdb in typeclasses eauto.Matthieu Sozeau
2015-02-23Partially porting eauto to the new tactic API.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-16Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
2015-01-15Add a (by default deactivated) option to force typeclass resolution toMatthieu Sozeau
2015-01-15Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-13TCs: Properly handle Hint Extern with conclusions of the form _ -> _Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-16Goal: remove some functions from the compatibility layer.Arnaud Spiwack
2014-10-15Fix for bug #3618.Matthieu Sozeau
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-15Avoid backtracking in typeclass search if a solution for a closedMatthieu Sozeau
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 05:03:18 +0000