From e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 7 Nov 2016 08:41:21 +0100
Subject: More explicit name for status of unification constraints.

---
 proofs/evar_refiner.ml | 2 +-
 proofs/pfedit.ml       | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f0cc73d2c..29cad06352 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 9c71e107cc..eddbf72a89 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);
 }
-- 
cgit v1.2.3