# Script simulating a dialog between coqide and coqtop -ideslave # Run it via fake_ide # # Simple backtrack by 2 before two global definitions # ADD { Definition foo := 0. } ADD { Definition bar := 1. } EDIT_AT initial QUERY { Fail Check foo. } QUERY { Fail Check bar. }