From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- test-suite/bugs/closed/shouldsucceed/1419.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 test-suite/bugs/closed/shouldsucceed/1419.v (limited to 'test-suite/bugs/closed/shouldsucceed/1419.v') diff --git a/test-suite/bugs/closed/shouldsucceed/1419.v b/test-suite/bugs/closed/shouldsucceed/1419.v new file mode 100644 index 00000000..d021107d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1419.v @@ -0,0 +1,8 @@ +Goal True. + set(a := 0). + set(b := a). + unfold a in b. + clear a. + Eval vm_compute in b. + trivial. +Qed. -- cgit v1.2.3