# Script simulating a dialog between coqide and coqtop -ideslave # Run it via fake_ide # # bug #2569 : Undoing inside modules # ADD { Module M. } ADD here { Definition x := 0. } ADD { End M. } EDIT_AT here # ADD { End M. } # QUERY { Check M.x. }