More explicit name for status of unification constraints.

5 files changed, 5 insertions, 5 deletions

diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 9fddede7e9..7fae328715 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -15,7 +15,7 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    leave P as subgoal or choose itself one solution *)
 
   intros. Fail refine (Cons (cast H _ y)).
-  Unset Use Unification Heuristics. (* Keep the unification constraint around *)
+  Unset Solve Unification Constraints. (* Keep the unification constraint around *)
   refine (Cons (cast H _ y)).
   intros.
   refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index f2cd41203c..f5a22bd508 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -651,4 +651,4 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
   Grab Existential Variables.
   subst_body; simpl.
   Fail refine (all_behead (projT2 _)).
-  Unset Use Unification Heuristics. refine (all_behead (projT2 _)).
+  Unset Solve Unification Constraints. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index afe8c62ed0..3189685ec0 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,4 +1,4 @@
 Goal exists x, x.
-Unset Use Unification Heuristics.
+Unset Solve Unification Constraints.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
index 01b9d158fe..684dba1961 100644
--- a/test-suite/bugs/closed/5149.v
+++ b/test-suite/bugs/closed/5149.v
@@ -40,7 +40,7 @@ Proof.
   Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
   solve [eapply interpf_SmartVarVar; subst; eassumption].
   Undo.
-  Unset Use Unification Heuristics.
+  Unset Solve Unification Constraints.
   (* User control of when constraints are solved *)
   solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
 Qed.
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c7fb82adac..b9413a4ac2 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,5 +1,5 @@
 (* Set Printing Existential Instances. *)
-Unset Use Unification Heuristics.
+Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =