aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/subtac_pretyping_F.ml
Commit message (Expand)AuthorAge
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* Fix obvious syntax error. Forgot to recompile before commiting...Gravatar msozeau2008-01-31
* Finish let| implementation and document itGravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Various little subtac fixes, add some useful tactics.Gravatar msozeau2007-02-19
* Fix matching on dependent types, taking a safe stand.Gravatar msozeau2007-02-12
* Various subtac fixes.Gravatar msozeau2007-01-15
* Subtac fixes, support for reasoning on wf defs.Gravatar msozeau2007-01-08
* Rework subtac pattern matching equalities generation.Gravatar msozeau2007-01-02
* Subtac bug fix, add list take example.Gravatar msozeau2006-12-08
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
* Suite commit polymorphismeGravatar herbelin2006-10-29
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Fix some nasty bug with the evars-to-dependent sum encoding.Gravatar msozeau2006-06-01
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29