diff options
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 04b98b1ac..b6c5da657 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 GroebnerR. +Require Export NsatzR. Open Scope R_scope. @@ -15,6 +15,6 @@ Lemma essai : Proof. intros. (* clear H. groebner used not to work when H was not cleared *) -groebnerR. +nsatzR. Qed. |