aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/extratactics.ml44
-rw-r--r--ltac/g_auto.ml42
-rw-r--r--ltac/tacinterp.ml8
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--tactics/tactics.ml2
-rw-r--r--test-suite/bugs/closed/2310.v2
-rw-r--r--test-suite/bugs/closed/3647.v2
-rw-r--r--test-suite/bugs/closed/4416.v2
-rw-r--r--test-suite/bugs/closed/5149.v2
-rw-r--r--test-suite/output/unifconstraints.v2
-rw-r--r--theories/Compat/Coq85.v2
14 files changed, 23 insertions, 23 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e6498e02b..2cca760c3 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ DECLARE PLUGIN "extratactics"
let with_delayed_uconstr ist c tac =
let flags = {
Pretyping.use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some Pfedit.solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true
@@ -342,7 +342,7 @@ END
let constr_flags = {
Pretyping.use_typeclasses = true;
- Pretyping.use_unif_heuristics = true;
+ Pretyping.solve_unification_constraints = true;
Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true }
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 8bc2ffd65..22a2d7fc2 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -43,7 +43,7 @@ END
let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some Pfedit.solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 08e67a0c2..b9dcc4e18 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -646,7 +646,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
let constr_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some solve_by_implicit_tactic;
fail_evar = true;
expand_evars = true }
@@ -661,21 +661,21 @@ let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true }
let open_constr_no_classes_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true }
let pure_open_constr_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = false;
expand_evars = false }
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 95d854323..4b6d10c64 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -243,7 +243,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;
- use_unif_heuristics : bool;
+ solve_unification_constraints : bool;
use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
@@ -339,7 +339,7 @@ let solve_remaining_evars flags env current_sigma pending =
if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
if Option.has_some flags.use_hook then
apply_inference_hook (Option.get flags.use_hook env) evdref pending;
- if flags.use_unif_heuristics then apply_heuristics env evdref false;
+ if flags.solve_unification_constraints then apply_heuristics env evdref false;
if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
!evdref
@@ -1109,14 +1109,14 @@ let ise_pretype_gen flags env sigma lvar kind c =
let default_inference_flags fail = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = fail;
expand_evars = true }
let no_classes_no_fail_inference_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = false;
expand_evars = true }
@@ -1180,7 +1180,7 @@ let understand_ltac flags env sigma lvar kind c =
let constr_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = true;
expand_evars = true }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eead48a54..0f3f7c3c9 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -51,7 +51,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;
- use_unif_heuristics : bool;
+ solve_unification_constraints : bool;
use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
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);
}
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 893f33f1a..e8cf09415 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1141,7 +1141,7 @@ let run_delayed env sigma c =
let tactic_infer_flags with_evar = {
Pretyping.use_typeclasses = true;
- Pretyping.use_unif_heuristics = true;
+ Pretyping.solve_unification_constraints = true;
Pretyping.use_hook = Some solve_by_implicit_tactic;
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 9fddede7e..7fae32871 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 f2cd41203..f5a22bd50 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 afe8c62ed..3189685ec 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 01b9d158f..684dba196 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 c7fb82ada..b9413a4ac 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 =
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index ba58e2d88..c64413383 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -29,4 +29,4 @@ Global Set Typeclasses Limit Intros.
Global Unset Typeclasses Filtered Unification.
(** Allow silently letting unification constraints float after a "." *)
-Global Unset Use Unification Heuristics. \ No newline at end of file
+Global Unset Solve Unification Constraints.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 03:20:16 +0000