From 5bb3ea7de91829c41e22c3e44f805bee06bc917a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 3 Apr 2017 09:06:27 +0200 Subject: Add test file for #4957. Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly". --- test-suite/bugs/closed/4957.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/4957.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/4957.v b/test-suite/bugs/closed/4957.v new file mode 100644 index 000000000..0efd87ac0 --- /dev/null +++ b/test-suite/bugs/closed/4957.v @@ -0,0 +1,6 @@ +Ltac get_value H := eval cbv delta [H] in H. + +Goal True. +refine (let X := _ in _). +let e := get_value X in unify e Prop. +Abort. -- cgit v1.2.3