From ccb173a440fa2eb7105a692c979253edbfe475ee Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 13:33:28 +0200 Subject: Unification constraint handling (#4763, #5149) Refine fix for bug #4763, fixing #5149 Tactic [Refine.solve_constraints] and global option Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of unification constraints and evar candidates to be solved. run_tactic now calls [solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics. The option allows to unset the forced solving unification constraints at each ".", letting the user control the places where the use of heuristics is done. Fix test-suite files too. --- proofs/pfedit.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a3ece1913..9c71e107c 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -13,6 +13,17 @@ open Entries open Environ 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.optread = (fun () -> !use_unification_heuristics_ref); + Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); +} + +let use_unification_heuristics () = !use_unification_heuristics_ref + let refining = Proof_global.there_are_pending_proofs let check_no_pending_proofs = Proof_global.check_no_pending_proof @@ -119,6 +130,11 @@ let solve ?with_end_tac gi info_lvl tac pr = | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac | Vernacexpr.SelectAll -> tac in + let tac = + if use_unification_heuristics () then + Proofview.tclTHEN tac Refine.solve_constraints + else tac + in let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in let () = match info_lvl with -- cgit v1.2.3 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. --- ltac/extratactics.ml4 | 4 ++-- ltac/g_auto.ml4 | 2 +- ltac/tacinterp.ml | 8 ++++---- pretyping/pretyping.ml | 10 +++++----- pretyping/pretyping.mli | 2 +- proofs/evar_refiner.ml | 2 +- proofs/pfedit.ml | 4 ++-- tactics/tactics.ml | 2 +- test-suite/bugs/closed/2310.v | 2 +- test-suite/bugs/closed/3647.v | 2 +- test-suite/bugs/closed/4416.v | 2 +- test-suite/bugs/closed/5149.v | 2 +- test-suite/output/unifconstraints.v | 2 +- theories/Compat/Coq85.v | 2 +- 14 files changed, 23 insertions(+), 23 deletions(-) (limited to 'proofs/pfedit.ml') 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. -- cgit v1.2.3