diff options
| author | Maxime Dénès | 2017-09-22 11:46:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-22 11:46:33 +0200 |
| commit | 06a723190858da8ed3f30736f22398aa7822c959 (patch) | |
| tree | 805ad45a4492a880dbf6008906eeaff807388ad0 /tools | |
| parent | 63b3b3f307053fd055355d8a669456c988d083aa (diff) | |
| parent | 569e8f7601ee1484f8373320a102fa2ab026078c (diff) | |
Merge PR #1055: Remove STM vernaculars
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/fake_ide.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index a9da27ba23..79723431cf 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -252,11 +252,9 @@ let eval_print l coq = let to_id, _ = get_id id in eval_call (query (0,(phrase, to_id))) coq | [ Tok(_,"WAIT") ] -> - let phrase = "Stm Wait." in - eval_call (query (0,(phrase,tip_id()))) coq + eval_call (wait ()) coq | [ Tok(_,"JOIN") ] -> - let phrase = "Stm JoinDocument." in - eval_call (query (0,(phrase,tip_id()))) coq + eval_call (status true) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" |