The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Have you tried defining [Local Ltac unfold_U := unfold U in *.] above your [Local Notation U := ...]?

Another thing you could do is make an [unhold_head] tactic that strips off arguments:
  Ltac unfold_head T :=
    idtac;
    lazymatch T with
      | ?f ?x => unfold_head f
      | _ => unfold T in *
    end.

-Jason

On Jun 5, 2015 8:08 AM, "Christian Doczkal" <doczkal AT ps.uni-saarland.de> wrote:

Hello Everyone,

I sometimes use "Local Notation" to hide arguments that remain constant
throughout a section. A contrived minimal example would look as follows:

Require Import ssreflect.

Definition U {T} (s : list T) := app s s.

Section Foo.
  Variables (T:Type) (x : T).
  Local Notation U := (U (cons x nil)).

  Lemma foo : length U = 1 -> False.

As a preprocessing step before calling an automation tactic, I want to
unfold all occurrences of U. However, using "unfold U in *" fails.
Ssreflect's "rewrite /U" succeeds in unfolding U, but requires explicit
naming of all hypothesis, which I'm trying to avoid.

  Lemma foo : length U = 1 -> False.
  Proof.
    intros H.
    (* unfold U in *. *)
    (* Error: U is bound to a notation that does not denote a reference. *)
    (* rewrite /U in * *)
    (* Error: assumptions should be named explicitly *)
    rewrite /U in H. (* unfolds (U (cons x nil)) *)
  Abort.

I tried using the following piece of Ltac:

Ltac unfold_U :=
(repeat progress match goal with
                  | [H : context[U] |- _] => rewrite /U in H
                 end); rewrite /U.

This works for the particular U defined above. If I try to abstract "U",
I get the same error as when calling "unfold U in *"

Is there anything else I can do? (This is on Coq 8.4)

--
Regards
Christian