From f6781defd922b80f8c48c4798c29644c99d5e611 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 13 Jun 2016 17:09:25 +0200
Subject: Print Assumptions and co. can "pierce opacity".

---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index e2acb10293..a81c2476de 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -83,7 +83,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
-- 
cgit v1.2.3


From ab1f43defa72e93617c3e3b09abb1876ff5a1b46 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 13 Jun 2016 17:09:47 +0200
Subject: STM classification: VernacTimeout may contain an "internal command".

---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index a81c2476de..3fe439cb20 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -99,7 +99,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))
-- 
cgit v1.2.3