diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 4 |
2 files changed, 3 insertions, 3 deletions
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); } |