aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
AgeCommit message (Expand)Author
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
2014-09-11Add a flag for restricting resolution of typeclasses toMatthieu Sozeau
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-06-24Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itPierre-Marie Pédrot
2014-06-23Clenvtac.unify is in the new monad.Pierre-Marie Pédrot
2014-06-21Reindex section variables for typeclass resolution if their type changed.Matthieu Sozeau
2014-05-06Various fixes of universe polymorphism and projections when they're set.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02A whole new implemenation of the refine tactic.aspiwack
2013-11-02A newly introduced variable inside a named context is no longer α-renamed.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-10-04Splitting Class_tactics between code and CAMLP4/5 declarations.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 12:19:47 +0000