 Permet a un unfold de recevoir ses occurences a travers une variable Ltac.  P.ex:     Tactic Notation "test" integer(i) := unfold plus at i  Ou meme:     Tactic Notation "test" ne_integer_list(i) := unfold plus at i  (voir commit 9159 d'Hugo).
 Permet a un unfold de recevoir ses occurences a travers une variable Ltac.
 P.ex:
    Tactic Notation "test" integer(i) := unfold plus at i
 Ou meme:
    Tactic Notation "test" ne_integer_list(i) := unfold plus at i
 (voir commit 9159 d'Hugo).



git-svn-id: a49b465eaba45b67e2e1e4e0b2c256a71f59fecb@9175 85f007b7-540e-0410-9357-904b9bb8a0f7

SamB/coq