aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/proofview.ml4
-rw-r--r--engine/proofview.mli1
-rw-r--r--ltac/extratactics.ml45
-rw-r--r--pretyping/unification.ml19
-rw-r--r--proofs/pfedit.ml16
-rw-r--r--proofs/refine.ml11
-rw-r--r--proofs/refine.mli5
-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/5149.v47
-rw-r--r--test-suite/output/unifconstraints.v1
12 files changed, 98 insertions, 21 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 855235d2b0..c01879765b 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 725445251d..90be2f90ab 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 d0318fb5f6..e6498e02b2 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 cec9f700af..fc63015a8e 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 a3ece19134..9c71e107cc 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 e5114a2eca..2f21428900 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 3d140f036b..a44632eff5 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 0be859eddf..9fddede7e9 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 495e67e09e..f2cd41203c 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 b97a8ce640..afe8c62ed0 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 0000000000..01b9d158fe
--- /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 c76fc74a0c..c7fb82adac 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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:22:34 +0000