aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_pretyping.ml
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-01-23Petit nettoyage faisant suite au commit #11847 .aspiwack
2008-08-21Various fixes w.r.t typeclasses and subtac: resolve tcs properly insidemsozeau
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-04-17Little fixes in setoid_rewrite.msozeau
2008-03-09Fix a few bugs in Program: use user-given typing constraints formsozeau
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
2008-01-04Add partial setoids in theories/Classes, add SetoidDec class for setoids with...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-10-24Fix some bugs, add possibility of automatically solving a proof statement's o...msozeau
2007-07-12Remove dead modules in Subtac.msozeau
2007-03-28Support for implicit formal argument types in Program ; parse types in type s...msozeau
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-02-23Debug wellfounded defs, work on cleaning obls envsmsozeau
2007-02-19Various little subtac fixes, add some useful tactics.msozeau
2007-01-15Various subtac fixes.msozeau
2006-11-09Support for mutual defs in obligation handling.msozeau
2006-10-31Work on obligation separation.msozeau
2006-10-26Facilities to automatically solve obligationsmsozeau
2006-09-01New handling of obligations.msozeau
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-07- Documentation of the Program tactics.msozeau
2006-03-22Subtac fixes, single fixpoint definitions are working again. Added a toggle o...msozeau
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau