aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.doc2
-rw-r--r--engine/evarutil.ml22
-rw-r--r--engine/evarutil.mli6
-rw-r--r--engine/proofview.ml36
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/pretyping.ml31
-rw-r--r--pretyping/unification.ml3
-rw-r--r--test-suite/Makefile12
-rw-r--r--test-suite/bugs/closed/4763.v13
-rw-r--r--test-suite/bugs/closed/5097.v7
10 files changed, 68 insertions, 66 deletions
diff --git a/Makefile.doc b/Makefile.doc
index aa6e478a8..cdd9852e8 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -124,7 +124,7 @@ endif
(cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`)
%.png: %.fig
- $(FIG2DEV) -m 2 -L png $< $@
+ $(FIG2DEV) -L png -m 2 $< $@
%.pdf: %.fig
$(FIG2DEV) -L pdftex $< $@
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e45e7dc49..df170c8dd 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -678,6 +678,28 @@ let gather_dependent_evars evm l =
(* /spiwack *)
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+ the current avatar of [g] (for instance [g] was changed by [clear]
+ into [g']). It returns [None] if [g] has been (partially)
+ solved. *)
+(* spiwack: [advance] is probably performance critical, and the good
+ behaviour of its definition may depend sensitively to the actual
+ definition of [Evd.find]. Currently, [Evd.find] starts looking for
+ a value in the heap of undefined variable, which is small. Hence in
+ the most common case, where [advance] is applied to an unsolved
+ goal ([advance] is used to figure if a side effect has modified the
+ goal) it terminates quickly. *)
+let rec advance sigma evk =
+ let evi = Evd.find sigma evk in
+ match evi.evar_body with
+ | Evar_empty -> Some evk
+ | Evar_defined v ->
+ if Option.default false (Store.get evi.evar_extra cleared) then
+ let (evk,_) = Term.destEvar v in
+ advance sigma evk
+ else
+ None
+
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c0c81442d..7fdc7aac7 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -110,6 +110,12 @@ val is_ground_env : evar_map -> env -> bool
its (partial) definition. *)
val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+ the current avatar of [g] (for instance [g] was changed by [clear]
+ into [g']). It returns [None] if [g] has been (partially)
+ solved. *)
+val advance : evar_map -> evar -> evar option
+
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 85a52fdca..208837f6a 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -152,33 +152,9 @@ let focus i j sp =
let (new_comb, context) = focus_sublist i j sp.comb in
( { sp with comb = new_comb } , context )
-
-(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
- the current avatar of [g] (for instance [g] was changed by [clear]
- into [g']). It returns [None] if [g] has been (partially)
- solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
- behaviour of its definition may depend sensitively to the actual
- definition of [Evd.find]. Currently, [Evd.find] starts looking for
- a value in the heap of undefined variable, which is small. Hence in
- the most common case, where [advance] is applied to an unsolved
- goal ([advance] is used to figure if a side effect has modified the
- goal) it terminates quickly. *)
-let rec advance sigma g =
- let open Evd in
- let evi = Evd.find sigma g in
- match evi.evar_body with
- | Evar_empty -> Some g
- | Evar_defined v ->
- if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
- let (e,_) = Term.destEvar v in
- advance sigma e
- else
- None
-
(** [undefined defs l] is the list of goals in [l] which are still
unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (advance defs) l
+let undefined defs l = CList.map_filter (Evarutil.advance defs) l
(** Unfocuses a proofview with respect to a context. *)
let unfocus c sp =
@@ -465,7 +441,7 @@ let iter_goal i =
Comb.get >>= fun initial ->
Proof.List.fold_left begin fun (subgoals as cur) goal ->
Solution.get >>= fun step ->
- match advance step goal with
+ match Evarutil.advance step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
@@ -489,7 +465,7 @@ let fold_left2_goal i s l =
in
Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
Solution.get >>= fun step ->
- match advance step goal with
+ match Evarutil.advance step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
@@ -533,7 +509,7 @@ let tclDISPATCHGEN0 join tacs =
let open Proof in
Pv.get >>= function
| { comb=[goal] ; solution } ->
- begin match advance solution goal with
+ begin match Evarutil.advance solution goal with
| None -> tclUNIT (join [])
| Some _ -> Proof.map (fun res -> join [res]) tac
end
@@ -1130,7 +1106,7 @@ module Goal = struct
Pv.get >>= fun step ->
let sigma = step.solution in
let map goal =
- match advance sigma goal with
+ match Evarutil.advance sigma goal with
| None -> None (** ppedrot: Is this check really necessary? *)
| Some goal ->
let gl =
@@ -1144,7 +1120,7 @@ module Goal = struct
let unsolved { self=self } =
tclEVARMAP >>= fun sigma ->
- tclUNIT (not (Option.is_empty (advance sigma self)))
+ tclUNIT (not (Option.is_empty (Evarutil.advance sigma self)))
(* compatibility *)
let goal { self=self } = self
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index d695d4537..f1526facc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1599,8 +1599,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
* ass.
*)
-(* This criterion relies on the fact that we postpone only problems of the form:
-?x [?x1 ... ?xn] = t or the symmetric case. *)
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)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 48bf9149d..6afa55862 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -249,17 +249,24 @@ type inference_flags = {
expand_evars : bool
}
-let frozen_holes (sigma, sigma') =
- (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
-
-let pending_holes (sigma, sigma') =
- let fold evk _ accu =
- if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
- in
- Evd.fold_undefined fold sigma' Evar.Set.empty
+(* Compute the set of still-undefined initial evars up to restriction
+ (e.g. clearing) and the set of yet-unsolved evars freshly created
+ in the extension [sigma'] of [sigma] (excluding the restrictions of
+ the undefined evars of [sigma] to be freshly created evars of
+ [sigma']). Otherwise said, we partition the undefined evars of
+ [sigma'] into those already in [sigma] or deriving from an evar in
+ [sigma] by restriction, and the evars properly created in [sigma'] *)
+
+let frozen_and_pending_holes (sigma, sigma') =
+ let add_derivative_of evk evi acc =
+ match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+ let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
+ let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+ let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+ (frozen,pending)
let apply_typeclasses env evdref frozen fail_evar =
- let filter_frozen = frozen in
+ let filter_frozen evk = Evar.Set.mem evk frozen in
evdref := Typeclasses.resolve_typeclasses
~filter:(if Flags.is_program_mode ()
then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -327,8 +334,7 @@ let check_evars_are_solved env current_sigma frozen pending =
(* Try typeclasses, hooks, unification heuristics ... *)
let solve_remaining_evars flags env current_sigma pending =
- let frozen = frozen_holes pending in
- let pending = pending_holes pending in
+ let frozen,pending = frozen_and_pending_holes pending in
let evdref = ref current_sigma in
if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
if Option.has_some flags.use_hook then
@@ -338,8 +344,7 @@ let solve_remaining_evars flags env current_sigma pending =
!evdref
let check_evars_are_solved env current_sigma pending =
- let frozen = frozen_holes pending in
- let pending = pending_holes pending in
+ let frozen,pending = frozen_and_pending_holes pending in
check_evars_are_solved env current_sigma frozen pending
let process_inference_flags flags env initial_sigma (sigma,c) =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 531b61553..e0a81cfbb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1269,7 +1269,8 @@ let solve_simple_evar_eqn ts env evd ev rhs =
match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
| UnifFailure (evd,reason) ->
error_cannot_unify env evd ~reason (mkEvar ev,rhs);
- | Success evd -> evd
+ | Success evd ->
+ Evarconv.consider_remaining_unif_problems env evd
(* [w_merge env sigma b metas evars] merges common instances in metas
or in evars, possibly generating new unification problems; if [b]
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b32071e80..10eb2df39 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -226,7 +226,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
fi; \
} > "$@"
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -257,7 +257,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
fi; \
} > "$@"
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -271,7 +271,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
fi; \
} > "$@"
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -330,7 +330,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
rm $$tmpexpected; \
} > "$@"
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -348,7 +348,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
# the .v file with exactly two digits after the dot. The reference for
# time is a 6120 bogomips cpu.
ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -379,7 +379,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
endif
# Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
deleted file mode 100644
index ae8ed0e6e..000000000
--- a/test-suite/bugs/closed/4763.v
+++ /dev/null
@@ -1,13 +0,0 @@
-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/5097.v b/test-suite/bugs/closed/5097.v
new file mode 100644
index 000000000..37b239cf6
--- /dev/null
+++ b/test-suite/bugs/closed/5097.v
@@ -0,0 +1,7 @@
+(* Tracing existing evars along the weakening rule ("clear") *)
+Goal forall y, exists x, x=0->x=y.
+intros.
+eexists ?[x].
+intros.
+let x:=constr:(ltac:(clear y; exact 0)) in idtac x.
+Abort.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 21:21:10 +0000