aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_pretyping_F.ml
AgeCommit message (Expand)Author
2008-01-31Fix obvious syntax error. Forgot to recompile before commiting...msozeau
2008-01-31Finish let| implementation and document itmsozeau
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-02-19Various little subtac fixes, add some useful tactics.msozeau
2007-02-12Fix matching on dependent types, taking a safe stand.msozeau
2007-01-15Various subtac fixes.msozeau
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
2007-01-02Rework subtac pattern matching equalities generation.msozeau
2006-12-08Subtac bug fix, add list take example.msozeau
2006-11-29Fork of cases impl for subtac.msozeau
2006-10-29Suite commit polymorphismeherbelin
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
2006-06-01Fix some nasty bug with the evars-to-dependent sum encoding.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau