diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 12:49:33 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-14 12:49:33 +0200 |
| commit | ee08817e76f91cc67ba9d2ea8f79218e413e21b4 (patch) | |
| tree | 95842d4a3cfd28da58ddfd8ad459e5697a53954d | |
| parent | 200974b1c6b7651577c3dd373520f023b651021a (diff) | |
| parent | ab1f43defa72e93617c3e3b09abb1876ff5a1b46 (diff) | |
Merge remote-tracking branch 'origin/pr/205' into trunk
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 358ff89b9..f312e8539 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -89,7 +89,7 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name () (* Commands piercing opaque *) let may_pierce_opaque = function - | { expr = VernacPrint (PrintName _) } -> true + | { expr = VernacPrint _ } -> true | { expr = VernacExtend (("Extraction",_), _) } -> true | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true @@ -105,7 +105,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e + | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e | _ -> false in if internal_command expr then begin prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) |