The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have long been annoyed that I could not recurse under binders in Ltac, and jumped through many hoops to fake it.  I recently discovered, that in Coq 8.5, this will be possible!  (And it already is in trunk, modulo a few bugs.)  I thought others in the Coq community might like to know this.

Here is some code that runs in trunk (and demos this feature and both bugs):

Ltac ret_and_left T :=
  let t := type of T in
  lazymatch eval hnf in t with
    | ?a /\ ?b => constr:(proj1 T)
    | forall x : ?T', @?f x =>
      let tac := ret_and_left in
      constr:(fun x : T' => $(let fx := constr:(T x) in
                              let t := tac fx in
                              exact t)$)
  end.

Goal forall A B : Prop, (A -> A -> A /\ B) -> True. intros. let t' := ret_and_left H in pose t'.

(* we get [a := fun _ x0 : A => proj1 (H x0 x0) : A -> A -> A]

we should get [a := fun x0 x1 : A => proj1 (H x0 x1) : A -> A -> A]. *)

-Jason