From 769debf970a354bbf71d924f89650028907fd832 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2019 12:03:55 -0800 Subject: [PATCH] fix: `is_unsafe` --- src/kernel/declaration.cpp | 2 +- stage0/src/kernel/declaration.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index c831406f38..50860e79f8 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -262,7 +262,7 @@ bool constant_info::is_unsafe() const { case constant_info_kind::Axiom: return to_axiom_val().is_unsafe(); case constant_info_kind::Definition: return to_definition_val().is_unsafe(); case constant_info_kind::Theorem: return false; - case constant_info_kind::Opaque: return false; + case constant_info_kind::Opaque: return to_opaque_val().is_unsafe(); case constant_info_kind::Quot: return false; case constant_info_kind::Inductive: return to_inductive_val().is_unsafe(); case constant_info_kind::Constructor: return to_constructor_val().is_unsafe(); diff --git a/stage0/src/kernel/declaration.cpp b/stage0/src/kernel/declaration.cpp index c831406f38..50860e79f8 100644 --- a/stage0/src/kernel/declaration.cpp +++ b/stage0/src/kernel/declaration.cpp @@ -262,7 +262,7 @@ bool constant_info::is_unsafe() const { case constant_info_kind::Axiom: return to_axiom_val().is_unsafe(); case constant_info_kind::Definition: return to_definition_val().is_unsafe(); case constant_info_kind::Theorem: return false; - case constant_info_kind::Opaque: return false; + case constant_info_kind::Opaque: return to_opaque_val().is_unsafe(); case constant_info_kind::Quot: return false; case constant_info_kind::Inductive: return to_inductive_val().is_unsafe(); case constant_info_kind::Constructor: return to_constructor_val().is_unsafe();