unfold.v « success « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/success/unfold.v

blob: 59adcff2372dd892c4189e7884cfb5882208800b (plain)

(* Test le Hint Unfold sur des var locales *)

Section toto.
Local EQ:=eq.
Goal (EQ nat O O).
Hints Unfold EQ.
Auto.
Save.