aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.doc2
-rw-r--r--ide/session.ml6
-rw-r--r--parsing/lexer.ml410
-rw-r--r--parsing/tok.ml2
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/evarutil.ml22
-rw-r--r--pretyping/evarutil.mli6
-rw-r--r--pretyping/pretyping.ml31
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/unification.ml3
-rw-r--r--proofs/proofview.ml36
-rw-r--r--tactics/tacinterp.ml3
-rw-r--r--test-suite/Makefile15
-rw-r--r--test-suite/bugs/closed/4763.v13
-rw-r--r--test-suite/bugs/closed/5097.v7
-rw-r--r--test-suite/output/ltac.out1
-rw-r--r--test-suite/output/ltac.v5
-rw-r--r--test-suite/success/Notations.v6
18 files changed, 100 insertions, 77 deletions
diff --git a/Makefile.doc b/Makefile.doc
index b7251ce579..cea6f9b1a5 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -61,7 +61,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/ide/session.ml b/ide/session.ml
index 168ddd4df9..711111139e 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -111,10 +111,10 @@ let set_buffer_handlers
let id = ref 0 in
fun () -> incr id; !id in
let running_action = ref None in
- let cancel_signal reason =
+ let cancel_signal ?(stop_emit=true) reason =
Minilib.log ("user_action cancelled: "^reason);
action_was_cancelled := true;
- GtkSignal.stop_emit () in
+ if stop_emit then GtkSignal.stop_emit () in
let del_mark () =
try buffer#delete_mark (`NAME "target")
with GText.No_such_mark _ -> () in
@@ -127,7 +127,7 @@ let set_buffer_handlers
fun () -> (* If Coq is busy due to the current action, we don't cancel *)
match !running_action with
| Some aid when aid = action -> ()
- | _ -> cancel_signal "Coq busy" in
+ | _ -> cancel_signal ~stop_emit:false "Coq busy" in
Coq.try_grab coqtop action fallback in
let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5d96873f31..cfea8793ac 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -495,7 +495,7 @@ let rec next_token = parser bp
| [< '' ' | '\t' | '\n' |'\r' as c; s >] ->
comm_loc bp; push_char c; next_token s
| [< ''$' as c; t = parse_after_special c bp >] ep ->
- comment_stop bp; (t, (ep, bp))
+ comment_stop bp; (t, (bp, ep))
| [< ''.' as c; t = parse_after_special c bp; s >] ep ->
comment_stop bp;
(* We enforce that "." should either be part of a larger keyword,
@@ -514,7 +514,7 @@ let rec next_token = parser bp
in
comment_stop bp; between_com := new_between_com; t
| [< ''?'; s >] ep ->
- let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
+ let t = parse_after_qmark bp s in comment_stop bp; (t, (bp, ep))
| [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
len = ident_tail (store 0 c); s >] ep ->
let id = get_buff len in
@@ -535,6 +535,12 @@ let rec next_token = parser bp
next_token s
| [< t = process_chars bp c >] -> comment_stop bp; t >] ->
t
+ | [< ' ('{' | '}' as c); s >] ep ->
+ let t,new_between_com =
+ if !between_com then (KEYWORD (String.make 1 c), (bp, ep)), true
+ else process_chars bp c s,false
+ in
+ comment_stop bp; between_com := new_between_com; t
| [< s >] ->
match lookup_utf8 s with
| Utf8Token (Unicode.Letter, n) ->
diff --git a/parsing/tok.ml b/parsing/tok.ml
index c96b53de41..25633c63d0 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -55,7 +55,7 @@ let to_string = function
| INT s -> Format.sprintf "INT %s" s
| STRING s -> Format.sprintf "STRING %S" s
| LEFTQMARK -> "LEFTQMARK"
- | BULLET s -> Format.sprintf "STRING %S" s
+ | BULLET s -> Format.sprintf "BULLET %S" s
| EOI -> "EOI"
let match_keyword kwd = function
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4a99246bba..d639208fb4 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1588,8 +1588,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/evarutil.ml b/pretyping/evarutil.ml
index 759e0e4d6d..9a9c946aeb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -600,6 +600,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/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f68651a74e..b60daae6d0 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -123,6 +123,12 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
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/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2e164e540a..c4ea79f954 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -183,17 +183,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))
@@ -244,8 +251,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
@@ -255,8 +261,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/reductionops.ml b/pretyping/reductionops.ml
index 7c7b31395e..9e654d29a1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -153,9 +153,6 @@ module Cst_stack = struct
let empty = []
let is_empty = CList.is_empty
- let sanity x y =
- assert(Term.eq_constr x y)
-
let drop_useless = function
| _ :: ((_,_,[])::_ as q) -> q
| l -> l
@@ -164,9 +161,9 @@ module Cst_stack = struct
let append2cst = function
| (c,params,[]) -> (c, h::params, [])
| (c,params,((i,t)::q)) when i = pred (Array.length t) ->
- let () = sanity h t.(i) in (c, params, q)
+ (c, params, q)
| (c,params,(i,t)::q) ->
- let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+ (c, params, (succ i,t)::q)
in
drop_useless (List.map append2cst cst_l)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b7edd6fcd6..9f8238513e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1244,7 +1244,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/proofs/proofview.ml b/proofs/proofview.ml
index 2fc4042354..46a370d530 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -146,33 +146,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 =
@@ -429,7 +405,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] >>
@@ -453,7 +429,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] >>
@@ -497,7 +473,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
@@ -1012,7 +988,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 =
@@ -1026,7 +1002,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/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5ecc46d670..c3f7fa1439 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -816,6 +816,9 @@ let rec message_of_value v =
Ftactic.return (pr_closed_glob_env (pf_env gl)
(Proofview.Goal.sigma gl) c)
end
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_id id) end
else match Value.to_list v with
| Some l ->
Ftactic.List.map message_of_value l >>= fun l ->
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f1cb21ecd5..491b16960e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -84,6 +84,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
# All subsystems
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
+PREREQUISITELOG = prerequisite/admit.v.log \
+ prerequisite/make_local.v.log prerequisite/make_notation.v.log
+
#######################################################################
# Phony targets
#######################################################################
@@ -221,7 +224,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 $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -253,7 +256,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 $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -267,7 +270,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 $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
rm $$tmpoutput; \
} > "$@"
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -307,7 +310,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 $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
@@ -338,7 +341,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 $(PREREQUISITELOG)
@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 ae8ed0e6e8..0000000000
--- 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 0000000000..37b239cf61
--- /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.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..266e4c7243 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,3 @@
The command has indeed failed with message:
Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Hx
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..e5bcff8ddb 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,8 @@ lazymatch goal with
| H1 : HT |- _ => idtac
end.
Abort.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2f7c62972a..511b60b4bb 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed.
(* Check absence of collision on ".." in nested notations with ".." *)
Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:59:04 +0000