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.
With Pierre 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 use of
subst, which in turns also has its quirks, making the mantra
inversion H; clear H; subst quite fragile. Furthermore,
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
destruct tactic, based on what he did during an internship (report in French (PDF)).