diff options
-rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index f1ff254f0..aaf3b3c1a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1633,12 +1633,17 @@ let collect_proof keep cur hd brkind id = let has_proof_no_using = function | Some (_, { expr = VernacProof(_,None) }) -> true | _ -> false in + let may_pierce_opaque = function + | { expr = VernacPrint (PrintName _) } -> true + | _ -> false in let parent = function Some (p, _) -> p | None -> assert false in let rec collect last accn id = let view = VCS.visit id in match view.step with + | (`Sideff (`Ast(x,_)) | `Cmd { cast = x }) + when may_pierce_opaque x -> `Sync(no_name,None,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next - | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next + | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) | `Alias _ -> `Sync (no_name,None,`Alias) | `Fork((_,_,_,_::_::_), _) -> @@ -1696,6 +1701,7 @@ let string_of_reason = function | `Doesn'tGuaranteeOpacity -> "not a simple opaque lemma" | `MutualProofs -> "block of mutually recursive proofs" | `Alias -> "contains Undo-like command" + | `Print -> "contains Print-like command" | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section" | `Unknown -> "unsupported case" |