The second OCaml-Paris meetup took place on May 21 at IRILL; I think it was a very interesting event, with good presentations on surprisingly diverse and interesting topics.
Boutillier, we have been working on a new Coq tactic lately, called
invert. From my point of view, it started as a quest to
build a replacement to the
inversion is a pain to use, as it generates sub-goals with
many (dependent) equalities that must be substituted, which force the
subst, which in turns also has its quirks, making
inversion H; clear H; subst quite fragile.
inversion has efficiency problems, being quite
slow and generating big proof terms. From Pierre’s point of view, this
work was a good way to implement a better
based on what he did during an internship (report
in French (PDF)).