diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-13 17:09:25 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-13 17:09:25 +0200 |
| commit | f6781defd922b80f8c48c4798c29644c99d5e611 (patch) | |
| tree | 2402da863e80e8703b7f645cfe5982d9768edacf | |
| parent | 36f95a197b106b928a3fc99d7ee5904099a654e4 (diff) | |
Print Assumptions and co. can "pierce opacity".
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e2acb1029..a81c2476d 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 |