Make the nsatz test-suite pass

3 files changed, 10 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/bug_5359.v b/test-suite/bugs/closed/bug_5359.v
index 1f202e4396..36f2ec5891 100644
--- a/test-suite/bugs/closed/bug_5359.v
+++ b/test-suite/bugs/closed/bug_5359.v
@@ -90,7 +90,7 @@ Goal False.
                                 (Ring_polynom.PEX Z 2)))
                           (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
                              (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
-    Nsatz.nsatz_compute
+    NsatzTactic.nsatz_compute
           (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
 
   let sugar := constr:( 0%Z ) in
@@ -214,6 +214,6 @@ Goal False.
                                    (Ring_polynom.PEX Z 2)))
                              (Ring_polynom.PEmul (Ring_polynom.PEX Z 3)
                                 (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
-    Nsatz.nsatz_compute
+    NsatzTactic.nsatz_compute
           (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
 Abort.
diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v
index aa0ac144c5..70180f47c7 100644
--- a/theories/nsatz/Nsatz.v
+++ b/theories/nsatz/Nsatz.v
@@ -34,6 +34,8 @@ Require Import ZArith.
 Require Import Lia.
 
 Require Export NsatzTactic.
+(** Make use of [discrR] in [nsatz] *)
+Ltac nsatz_internal_discrR ::= discrR.
 
 (* Real numbers *)
 Require Import Reals.
diff --git a/theories/nsatz/NsatzTactic.v b/theories/nsatz/NsatzTactic.v
index 79253009f4..db7dab2c46 100644
--- a/theories/nsatz/NsatzTactic.v
+++ b/theories/nsatz/NsatzTactic.v
@@ -29,7 +29,6 @@ Require Export Ncring.
 Require Export Ncring_initial.
 Require Export Ncring_tac.
 Require Export Integral_domain.
-Require Import DiscrR.
 Require Import ZArith.
 Require Import Lia.
 
@@ -347,6 +346,11 @@ Ltac get_lpol g :=
        let l := get_lpol g in constr:(p::l)
   end.
 
+(** We only make use of [discrR] if [nsatz] support for reals is
+    loaded.  To do this, we redefine this tactic in Nsatz.v to make
+    use of real discrimination. *)
+Ltac nsatz_internal_discrR := idtac.
+
 Ltac nsatz_generic radicalmax info lparam lvar :=
  let nparam := eval compute in (Z.of_nat (List.length lparam)) in
  match goal with
@@ -414,7 +418,7 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
             try exact integral_domain_minus_one_zero
           || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
                      one, one_notation, multiplication, mul_notation, zero, zero_notation;
-                     discrR || lia ])
+                     nsatz_internal_discrR || lia ])
           || ((*simpl*) idtac) || idtac "could not prove discrimination result"
         ]
       ]