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