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 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. |