aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-11-07 08:42:17 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-11-07 09:11:47 +0100
commit6f30019bfd99a0125fdc12baf8b6c04169701fb7 (patch)
tree9fd11119bcf4f4c51baa91de114c246299ddc855
parent207fcfd9355b01441f2a01614a7de017f4148cde (diff)
parente6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c (diff)
Merge commit 'e6edb33' into v8.6
Was PR#331: Solve_constraints and Set Use Unification Heuristics
-rw-r--r--engine/proofview.ml4
-rw-r--r--engine/proofview.mli1
-rw-r--r--ltac/extratactics.ml49
-rw-r--r--ltac/g_auto.ml42
-rw-r--r--ltac/tacinterp.ml8
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
-rw-r--r--plugins/ssrmatching/ssrmatching.mli2
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarconv.mli3
-rw-r--r--pretyping/evarsolve.ml6
-rw-r--r--pretyping/evarsolve.mli3
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/unification.ml27
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/pfedit.ml16
-rw-r--r--proofs/refine.ml11
-rw-r--r--proofs/refine.mli5
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/equality.ml3
-rw-r--r--tactics/tactics.ml2
-rw-r--r--test-suite/bugs/closed/2310.v6
-rw-r--r--test-suite/bugs/closed/3647.v3
-rw-r--r--test-suite/bugs/closed/4416.v1
-rw-r--r--test-suite/bugs/closed/4763.v13
-rw-r--r--test-suite/bugs/closed/5149.v47
-rw-r--r--test-suite/bugs/closed/HoTT_coq_117.v21
-rw-r--r--test-suite/output/unifconstraints.v1
-rw-r--r--theories/Compat/Coq85.v3
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/vernacentries.ml2
31 files changed, 178 insertions, 51 deletions
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..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 }
@@ -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/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 52208979c..20dbc2be4 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/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index cf9a42945..ef04bef8e 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -354,7 +354,7 @@ let nf_open_term sigma0 ise c =
!s', Evd.evar_universe_context s, c'
let unif_end env sigma0 ise0 pt ok =
- let ise = Evarconv.consider_remaining_unif_problems env ise0 in
+ let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
let s, uc, t = nf_open_term sigma0 ise pt in
let ise1 = create_evar_defs s in
let ise1 = Evd.set_universe_context ise1 uc in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 74a603e51..288a04e60 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -213,7 +213,7 @@ val assert_done : 'a option ref -> 'a
(** Very low level APIs.
these are calls to evarconv's [the_conv_x] followed by
- [consider_remaining_unif_problems] and [resolve_typeclasses].
+ [solve_unif_constraints_with_heuristics] and [resolve_typeclasses].
In case of failure they raise [NoMatch] *)
val unify_HO : env -> evar_map -> constr -> constr -> evar_map
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28600ad15..9fd55a488 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1081,7 +1081,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
match evar_conv_x ts env_evar evd CUMUL idty evty with
| UnifFailure _ -> error "Cannot find an instance"
| Success evd ->
- match reconsider_conv_pbs (evar_conv_x ts) evd with
+ match reconsider_unif_constraints (evar_conv_x ts) evd with
| UnifFailure _ -> error "Cannot find an instance"
| Success evd ->
evd
@@ -1213,7 +1213,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
let conv_algo = evar_conv_x ts in
let evd = check_evar_instance evd evk a conv_algo in
let evd = Evd.define evk a evd in
- match reconsider_conv_pbs conv_algo evd with
+ match reconsider_unif_constraints conv_algo evd with
| Success evd -> solve_unconstrained_evars_with_candidates ts evd
| UnifFailure _ -> aux l
with
@@ -1236,7 +1236,7 @@ let solve_unconstrained_impossible_cases env evd =
Evd.define evk ty evd'
| _ -> evd') evd evd
-let consider_remaining_unif_problems env
+let solve_unif_constraints_with_heuristics env
?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd =
let evd = solve_unconstrained_evars_with_candidates ts evd in
let rec aux evd pbs progress stuck =
@@ -1266,6 +1266,8 @@ let consider_remaining_unif_problems env
check_problems_are_solved env heuristic_solved_evd;
solve_unconstrained_impossible_cases env heuristic_solved_evd
+let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics
+
(* Main entry points *)
exception UnableToUnify of evar_map * unification_error
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 14947c892..2231e5bc3 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -33,7 +33,10 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
(** Try heuristics to solve pending unification problems and to solve
evars with candidates *)
+val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
+
val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
+(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
(** Check all pending unification problems are solved and raise an
error otherwise *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f1526facc..f0aa9b564 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1603,7 +1603,7 @@ let status_changed lev (pbty,_,t1,t2) =
(try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
(try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
-let reconsider_conv_pbs conv_algo evd =
+let reconsider_unif_constraints conv_algo evd =
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
List.fold_left
(fun p (pbty,env,t1,t2 as x) ->
@@ -1616,6 +1616,8 @@ let reconsider_conv_pbs conv_algo evd =
(Success evd)
pbs
+let reconsider_conv_pbs = reconsider_unif_constraints
+
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
* Returns an optional list of evars that were instantiated, or None
@@ -1626,7 +1628,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
try
let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
- reconsider_conv_pbs conv_algo evd
+ reconsider_unif_constraints conv_algo evd
with
| NotInvertibleUsingOurAlgorithm t ->
UnifFailure (evd,NotClean (ev1,env,t))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index f94c83b6d..b6bdc0788 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -54,7 +54,10 @@ val solve_evar_evar : ?force:bool ->
val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
bool option * existential * constr -> unification_result
+val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
+
val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
+(** @deprecated Alias for [reconsider_unif_constraints] *)
val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
constr -> constr list option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6afa55862..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
@@ -290,7 +290,7 @@ let apply_inference_hook hook evdref pending =
let apply_heuristics env evdref fail_evar =
(* Resolve eagerly, potentially making wrong choices *)
- try evdref := consider_remaining_unif_problems
+ try evdref := solve_unif_constraints_with_heuristics
~ts:(Typeclasses.classes_transparent_state ()) env !evdref
with e when CErrors.noncritical e ->
let e = CErrors.push e in if fail_evar then iraise e
@@ -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/pretyping/unification.ml b/pretyping/unification.ml
index e0a81cfbb..259318693 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1220,7 +1220,7 @@ let is_mimick_head ts f =
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
- let evd' = Evarconv.consider_remaining_unif_problems env evd' in
+ let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
(evd',j'.uj_val)
@@ -1270,7 +1270,11 @@ let solve_simple_evar_eqn ts env evd ev rhs =
| UnifFailure (evd,reason) ->
error_cannot_unify env evd ~reason (mkEvar ev,rhs);
| Success evd ->
- Evarconv.consider_remaining_unif_problems env evd
+ if Flags.version_less_or_equal Flags.V8_5 then
+ (* We used to force solving unrelated problems at arbitrary times *)
+ Evarconv.solve_unif_constraints_with_heuristics env evd
+ else (* solve_simple_eqn calls reconsider_unif_constraints itself *)
+ evd
(* [w_merge env sigma b metas evars] merges common instances in metas
or in evars, possibly generating new unification problems; if [b]
@@ -1297,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' =
@@ -1393,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
@@ -1452,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
@@ -1881,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/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 a3ece1913..eddbf72a8 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 = "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);
+}
+
+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..3f5527060 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.solve_unif_constraints_with_heuristics 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/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 51bf69e5c..af1ab4197 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1440,7 +1440,7 @@ let initial_select_evars filter =
let resolve_typeclass_evars debug depth unique env evd filter split fail =
let evd =
- try Evarconv.consider_remaining_unif_problems
+ try Evarconv.solve_unif_constraints_with_heuristics
~ts:(Typeclasses.classes_transparent_state ()) env evd
with e when CErrors.noncritical e -> evd
in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e9d08d737..bb3cbad92 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let dflt_typ = unsafe_type_of env sigma dflt in
try
let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
- let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
+ let () =
+ evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
dflt
with Evarconv.UnableToUnify _ ->
error "Cannot solve a unification problem."
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index af52c5237..db19d54bd 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 0be859edd..7fae32871 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 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 495e67e09..f5a22bd50 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 Solve Unification Constraints. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce64..3189685ec 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
Goal exists x, x.
+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/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/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 000000000..684dba196
--- /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 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/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. *)
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0..b9413a4ac 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
(* Set Printing Existential Instances. *)
+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 1bc6fee0c..64ba6b1e3 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -31,3 +31,6 @@ Global Set Refolding Reduction.
Global Set Typeclasses Legacy Resolution.
Global Set Typeclasses Limit Intros.
Global Unset Typeclasses Filtered Unification.
+
+(** Allow silently letting unification constraints float after a "." *)
+Global Unset Solve Unification Constraints.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 12c387dcf..7ffe680e5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1129,7 +1129,7 @@ let interp_recursive isfix fixl notations =
() in
(* Instantiate evars and check all are resolved *)
- let evd = consider_remaining_unif_problems env_rec !evdref in
+ let evd = solve_unif_constraints_with_heuristics env_rec !evdref in
let evd, nf = nf_evars_and_universes evd in
let fixdefs = List.map (Option.map nf) fixdefs in
let fixtypes = List.map nf fixtypes in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8a28d979c..68485231b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1573,7 +1573,7 @@ let get_current_context_of_args = function
let vernac_check_may_eval redexp glopt rc =
let (sigma, env) = get_current_context_of_args glopt in
let sigma', c = interp_open_constr env sigma rc in
- let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
+ let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
Evarconv.check_problems_are_solved env sigma';
let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
let pl, uctx = Evd.universe_context sigma' in