From 4a96fefd96e9786e44e216ab19d4b91c0bc2451a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Aug 2014 17:25:39 -0700 Subject: [PATCH] fix(library/unifier): bug in unifier priority queue Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 6 ++++++ tests/lean/interactive/test_single.sh | 1 + tests/lean/run/coe7.lean | 11 +++++++++++ 3 files changed, 18 insertions(+) create mode 100644 tests/lean/run/coe7.lean diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 6acd27cbf..5ad2c11fa 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1892,6 +1892,12 @@ struct unifier_fn { return process_delta(c); } else if (modified) { return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification(), relax_main_opaque(c)); + } else if (auto d = is_owned(c)) { + // Metavariable in the constraint is owned by choice constraint. + // choice constraint was postponed... since c was not modifed + // So, we should postpone this one too. + add_cnstr(c, to_cnstr_group(*d+1)); + return true; } else if (is_flex_rigid(c)) { return process_flex_rigid(c); } else if (is_flex_flex(c)) { diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh index a91ecf409..a739e0690 100755 --- a/tests/lean/interactive/test_single.sh +++ b/tests/lean/interactive/test_single.sh @@ -5,6 +5,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then fi ulimit -s unlimited LEAN=$1 +export LEAN_PATH=../../../library/standard:. if [ $# -ne 3 ]; then INTERACTIVE=no else diff --git a/tests/lean/run/coe7.lean b/tests/lean/run/coe7.lean new file mode 100644 index 000000000..8c000c9a0 --- /dev/null +++ b/tests/lean/run/coe7.lean @@ -0,0 +1,11 @@ +import logic + +variable nat : Type.{1} +variable int : Type.{1} +variable of_nat : nat → int +coercion of_nat + +theorem tst (n : nat) : n = n := +have H : true, from trivial, +calc n = n : refl _ + ... = n : refl _ \ No newline at end of file