diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-26 10:45:38 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-26 10:45:38 +0100 |
| commit | 2ef5fa7910e644d7eb39ee01024878a67086bd42 (patch) | |
| tree | b644a5435d31a1440e2b7c62c47f4aed14dbfe68 | |
| parent | 1bafb18f64ab1c929abfaf9c1b75f691914d9a46 (diff) | |
STM: change how proof mode switching commands are handled (decl_mode)
This is likely to make nested proofs containing proof modes switch
broken, but fixes the problems Arnaud has in his branch.
It is possible that the classification function we have today
is not fine grained enough.
If a command that changes the proof mode has as the only global
effect changing the proof mode, then the current code is fine.
If it has a more global effect that persists after the proof is over
but has no impact on the proof itself, then the old code is fine.
As far as I can get, the proof mode switching commands have
a global effect (changing parser) but also a proof effect
(un/focusing). We don't have a classification for these.
Today a command having a global effect is played twice:
on the proof branch an on master. Of course if such command
cannot work on master (where there is no finished proof for
example) we need a special treatment for it.
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 267f08ed5..9e30cbbcd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2126,9 +2126,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue}); - VCS.propagate_sideff (Some x); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () |