diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-19 13:33:28 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-22 11:32:06 +0200 |
commit | ccb173a440fa2eb7105a692c979253edbfe475ee (patch) | |
tree | 4b1dc0c82e3da6b1219adcc195aa6626d5ae3d74 /proofs/pfedit.ml | |
parent | 379c2403b1cd031091a2271353f26ab24afeb1e5 (diff) |
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.
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r-- | proofs/pfedit.ml | 16 |
1 files changed, 16 insertions, 0 deletions
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 |