diff options
| author | Maxime Dénès | 2016-04-12 18:59:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-04-12 19:05:30 +0200 |
| commit | 927e88de465e94bf18b970b45faaf97b4c2dff82 (patch) | |
| tree | 9519903aa6cf53dcb1de1958ecaf9b5045469738 | |
| parent | 2bd36760f84f1d79af63cdee4d5d53f289a51204 (diff) | |
Quick fix for #4603 (part 2): Anomaly: Universe undefined
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4603.v | 10 |
2 files changed, 15 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index a6d119f0cd..094457431e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2250,7 +2250,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue}); - VCS.propagate_sideff (Some x); + let replay = match x.expr with + | VernacDefinition(_, _, DefineBody _) -> None + | _ -> Some x + in + VCS.propagate_sideff replay; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v new file mode 100644 index 0000000000..e7567623a6 --- /dev/null +++ b/test-suite/bugs/closed/4603.v @@ -0,0 +1,10 @@ +Axiom A : Type. + +Goal True. exact I. +Check (fun P => P A). +Abort. + +Goal True. +Definition foo (A : Type) : Prop:= True. + set (x:=foo). split. +Qed.
\ No newline at end of file |