More explicit name for status of unification constraints.

2 files changed, 3 insertions, 3 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f0cc73d2..29cad0635 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -46,7 +46,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
   let sigma',typed_c =
     let flags = {
       Pretyping.use_typeclasses = true;
-      Pretyping.use_unif_heuristics = true;
+      Pretyping.solve_unification_constraints = true;
       Pretyping.use_hook = None;
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9c71e107c..eddbf72a8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -16,8 +16,8 @@ open Evd
 let use_unification_heuristics_ref = ref true
 let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
-  Goptions.optname = "Unification heuristics are applied at every .";
-  Goptions.optkey = ["Use";"Unification";"Heuristics"];
+  Goptions.optname = "Solve unification constraints at every \".\"";
+  Goptions.optkey = ["Solve";"Unification";"Constraints"];
   Goptions.optread = (fun () -> !use_unification_heuristics_ref);
   Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a);
 }