From 0509cfcf99dd3e5a741aea050b4a84d5ebf9bf62 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 17 Jan 2019 18:51:59 +0100 Subject: [PATCH] fix(frontends/lean/vm_elaborator): name to obj --- src/frontends/lean/vm_elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index 483f6c882a..28a644630a 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -433,7 +433,7 @@ vm_obj to_obj(name const & n) { } else if (n.is_string()) { return mk_vm_constructor(1, to_obj(n.get_prefix()), to_obj(n.get_string().to_std_string())); } else { - return mk_vm_constructor(1, to_obj(n.get_prefix()), mk_vm_nat(n.get_numeral().to_mpz())); + return mk_vm_constructor(2, to_obj(n.get_prefix()), mk_vm_nat(n.get_numeral().to_mpz())); } }