From 379c2403b1cd031091a2271353f26ab24afeb1e5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 22 Oct 2016 10:17:39 +0200 Subject: Port fix for bugs 4763, 5149, previously 0b417c12e Adds a compatibility flag so that the behavior of 8.5 can be obtained too. Original commit: unification.ml: fix for bug #4763, unif regression Do not force all remaining conversions problems to be solved after the _first_ solution of an evar. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too. --- test-suite/bugs/closed/4763.v | 13 +++++++++++++ test-suite/bugs/closed/HoTT_coq_117.v | 21 ++++++++++++++++++++- 2 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4763.v (limited to 'test-suite/bugs/closed') diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v new file mode 100644 index 000000000..ae8ed0e6e --- /dev/null +++ b/test-suite/bugs/closed/4763.v @@ -0,0 +1,13 @@ +Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. +Coercion is_true : bool >-> Sortclass. +Global Instance: Transitive leb. +Admitted. + +Goal forall x y z, leb x y -> leb y z -> True. + intros ??? H H'. + lazymatch goal with + | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] + => pose proof (transitivity H H' : is_true (R x z)) + end. + exact I. +Qed. \ No newline at end of file diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v index 5fbcfef4e..de60fd0ae 100644 --- a/test-suite/bugs/closed/HoTT_coq_117.v +++ b/test-suite/bugs/closed/HoTT_coq_117.v @@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, Admitted. Inductive Empty : Set := . -Instance contr_from_Empty {_ : Funext} (A : Type) : +Fail Instance contr_from_Empty {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect _ x)). + +Fail Instance contr_from_Empty {F : Funext} (A : Type) : Contr_internal (Empty -> A) := BuildContr _ (Empty_rect (fun _ => A)) (fun f => path_forall _ f (fun x => Empty_rect _ x)). + +(** This could be disallowed, this uses the Funext argument *) +Instance contr_from_Empty {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)). + +Instance contr_from_Empty' {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)). (* Toplevel input, characters 15-220: Anomaly: unknown meta ?190. Please report. *) -- cgit v1.2.3 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. --- engine/proofview.ml | 4 ---- engine/proofview.mli | 1 - ltac/extratactics.ml4 | 5 ++++ pretyping/unification.ml | 19 ++++----------- proofs/pfedit.ml | 16 +++++++++++++ proofs/refine.ml | 11 +++++++++ proofs/refine.mli | 5 ++++ test-suite/bugs/closed/2310.v | 6 ++++- test-suite/bugs/closed/3647.v | 3 ++- test-suite/bugs/closed/4416.v | 1 + test-suite/bugs/closed/5149.v | 47 +++++++++++++++++++++++++++++++++++++ test-suite/output/unifconstraints.v | 1 + 12 files changed, 98 insertions(+), 21 deletions(-) create mode 100644 test-suite/bugs/closed/5149.v (limited to 'test-suite/bugs/closed') diff --git a/engine/proofview.ml b/engine/proofview.ml index 855235d2b..c01879765 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1157,10 +1157,6 @@ let tclLIFT = Proof.lift let tclCHECKINTERRUPT = tclLIFT (NonLogical.make Control.check_for_interrupt) - - - - (*** Compatibility layer with <= 8.2 tactics ***) module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma diff --git a/engine/proofview.mli b/engine/proofview.mli index 725445251..90be2f90a 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -373,7 +373,6 @@ val mark_as_unsafe : unit tactic with given up goals cannot be closed. *) val give_up : unit tactic - (** {7 Control primitives} *) (** [tclPROGRESS t] checks the state of the proof after [t]. It it is diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d0318fb5f..e6498e02b 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -370,6 +370,11 @@ TACTIC EXTEND simple_refine | [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ] END +(* Solve unification constraints using heuristics or fail if any remain *) +TACTIC EXTEND solve_constraints +[ "solve_constraints" ] -> [ Refine.solve_constraints ] +END + (**********************************************************************) (* Inversion lemmas (Leminv) *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cec9f700a..fc63015a8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1301,7 +1301,6 @@ let w_merge env with_types flags (evd,metas,evars) = if is_mimick_head flags.modulo_delta f then let evd' = mimick_undefined_evar evd flags f (Array.length cl) evk in - (* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *) w_merge_rec evd' metas evars eqns else let evd' = @@ -1397,8 +1396,7 @@ let w_merge env with_types flags (evd,metas,evars) = (* Assign evars in the order of assignments during unification *) (List.rev evars) [] in - if with_types then check_types res - else res + if with_types then check_types res else res let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = let metas,evd = retract_coercible_metas evd in @@ -1456,7 +1454,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let subst = Array.fold_left2 fold_subst subst l1 l2 in let evd = w_merge env true flags.merge_unify_flags subst in try_resolve_typeclasses env evd flags.resolve_evars - (mkApp(f1,l1)) (mkApp(f2,l2)) + (mkApp(f1,l1)) (mkApp(f2,l2)) (* takes a substitution s, an open term op and a closed term cl try to find a subterm of cl which matches op, if op is just a Meta @@ -1885,21 +1883,14 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; w_merge env false flags.merge_unify_flags - (evd',[p,pred,(Conv,TypeProcessed)],[]) - - (* let evd',metas,evars = *) - (* try unify_0 env evd' CUMUL flags predtyp typp *) - (* with NotConvertible -> *) - (* error_wrong_abstraction_type env evd *) - (* (Evd.meta_name evd p) pred typp predtyp *) - (* in *) - (* w_merge env false flags (evd',(p,pred,(Conv,TypeProcessed))::metas,evars) *) + (evd',[p,pred,(Conv,TypeProcessed)],[]) let secondOrderDependentAbstraction env evd flags typ (p, oplist) = let typp = Typing.meta_type evd p in let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in w_merge env false flags.merge_unify_flags - (evd,[p,pred,(Conv,TypeProcessed)],[]) + (evd,[p,pred,(Conv,TypeProcessed)],[]) + let secondOrderAbstractionAlgo dep = if dep then secondOrderDependentAbstraction else secondOrderAbstraction 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 diff --git a/proofs/refine.ml b/proofs/refine.ml index e5114a2ec..2f2142890 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -149,3 +149,14 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> } in refine ?unsafe f end } + +(** {7 solve_constraints} + + Ensure no remaining unification problems are left. Run at every "." by default. *) + +let solve_constraints = + let open Proofview in + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> + try let sigma = Evarconv.consider_remaining_unif_problems env sigma in + Unsafe.tclEVARSADVANCE sigma + with e -> tclZERO e diff --git a/proofs/refine.mli b/proofs/refine.mli index 3d140f036..a44632eff 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -43,3 +43,8 @@ val with_type : Environ.env -> Evd.evar_map -> val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) + +(** {7 Unification constraint handling} *) + +val solve_constraints : unit tactic +(** Solve any remaining unification problems, applying heuristics. *) diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v index 0be859edd..9fddede7e 100644 --- a/test-suite/bugs/closed/2310.v +++ b/test-suite/bugs/closed/2310.v @@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either leave P as subgoal or choose itself one solution *) -intros. refine (Cons (cast H _ y)). \ No newline at end of file + intros. Fail refine (Cons (cast H _ y)). + Unset Use Unification Heuristics. (* 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 495e67e09..f2cd41203 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -650,4 +650,5 @@ Goal forall (ptest : program) (cond : Condition) (value : bool) Grab Existential Variables. subst_body; simpl. - refine (all_behead (projT2 _)). + Fail refine (all_behead (projT2 _)). + Unset Use Unification Heuristics. refine (all_behead (projT2 _)). diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v index b97a8ce64..afe8c62ed 100644 --- a/test-suite/bugs/closed/4416.v +++ b/test-suite/bugs/closed/4416.v @@ -1,3 +1,4 @@ Goal exists x, x. +Unset Use Unification Heuristics. 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 new file mode 100644 index 000000000..01b9d158f --- /dev/null +++ b/test-suite/bugs/closed/5149.v @@ -0,0 +1,47 @@ +Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x. +intros. +eexists. +rewrite <- H. +eassumption. +Qed. + +Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) + (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : +flat_type -> Type) + (v v' : interp_flat_type1 t'), + v = v' -> + forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0) + (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> +interp_flat_type0 t0) + (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t)) + (x' : interp_flat_type1 (Tbase t)) (T : Type) + (flatten_binding_list : forall t0 : flat_type, + interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T) + (P : T -> list T -> Prop) (prod : Type -> Type -> Type) + (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) +(interp_flat_type1 (Tbase x0)) -> T) + (pair : forall A B : Type, A -> B -> prod A B), + P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x')) + (flatten_binding_list t' (SmartVarVar t' v') v) -> + (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 +t'0) + (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)), + P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 +x'0)) + (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf +(Tbase t0) x0 = x'0) -> + interpf (Tbase t) x = x'. +Proof. + intros ?????????????????????? interpf_SmartVarVar. + solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail +"too early". + Undo. + (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) + Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ]. + solve [eapply interpf_SmartVarVar; subst; eassumption]. + Undo. + Unset Use Unification Heuristics. + (* 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 c76fc74a0..c7fb82ada 100644 --- a/test-suite/output/unifconstraints.v +++ b/test-suite/output/unifconstraints.v @@ -1,4 +1,5 @@ (* Set Printing Existential Instances. *) +Unset Use Unification Heuristics. Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat. Goal True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = -- 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 'test-suite/bugs/closed') 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