From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- test-suite/bugs/closed/shouldsucceed/2145.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test-suite/bugs/closed/shouldsucceed/2145.v') diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v index b6c5da65..4dc0de74 100644 --- a/test-suite/bugs/closed/shouldsucceed/2145.v +++ b/test-suite/bugs/closed/shouldsucceed/2145.v @@ -1,7 +1,7 @@ (* Test robustness of Groebner tactic in presence of disequalities *) Require Export Reals. -Require Export NsatzR. +Require Export Nsatz. Open Scope R_scope. @@ -15,6 +15,6 @@ Lemma essai : Proof. intros. (* clear H. groebner used not to work when H was not cleared *) -nsatzR. +nsatz. Qed. -- cgit v1.2.3