diff options
author | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /test-suite/bugs/closed/shouldsucceed/2145.v | |
parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2145.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2145.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |