From 41643d64007ed6fddbb64335b6097b2f1073e354 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 3 Nov 2016 18:38:07 -0400 Subject: [PATCH] fix(library/compiler/vm_compiler): prevent segfault --- src/library/compiler/vm_compiler.cpp | 1 + tests/lean/run/declare_axiom.lean | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 tests/lean/run/declare_axiom.lean diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 48b3cfb1fc..5e6973630a 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -335,6 +335,7 @@ environment vm_compile(environment const & env, buffer> const & } environment vm_compile(environment const & env, declaration const & d) { + if (!d.is_definition()) return env; buffer> procs; preprocess(env, d, procs); return vm_compile(env, procs); diff --git a/tests/lean/run/declare_axiom.lean b/tests/lean/run/declare_axiom.lean new file mode 100644 index 0000000000..cc8443f84b --- /dev/null +++ b/tests/lean/run/declare_axiom.lean @@ -0,0 +1,5 @@ +open tactic + +run_command (do + e ← to_expr `(false), + add_decl $ declaration.ax `useful_assumption [] e)