aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evd.ml179
-rw-r--r--engine/evd.mli4
-rw-r--r--interp/constrextern.ml5
-rw-r--r--lib/system.ml10
-rw-r--r--library/universes.ml4
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/evarutil.ml9
-rw-r--r--pretyping/typeclasses.ml11
-rw-r--r--pretyping/unification.ml4
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/goal.ml5
-rw-r--r--proofs/proofview.ml5
-rw-r--r--stm/stm.ml12
-rw-r--r--test-suite/bugs/closed/3068.v2
-rw-r--r--test-suite/output/Existentials.out3
-rw-r--r--test-suite/output/Notations.out14
-rw-r--r--test-suite/output/inference.out8
-rw-r--r--test-suite/success/Injection.v2
-rw-r--r--test-suite/success/apply.v2
-rw-r--r--test-suite/success/destruct.v8
-rw-r--r--toplevel/himsg.ml2
21 files changed, 181 insertions, 115 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 8f8b29d10..bcbf99e87 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -208,15 +208,6 @@ let map_evar_info f evi =
evar_concl = f evi.evar_concl;
evar_candidates = Option.map (List.map f) evi.evar_candidates }
-let evar_ident_info evi =
- match evi.evar_source with
- | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
- | _,Evar_kinds.VarInstance id -> id
- | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
- | _ ->
- let env = reset_with_named_context evi.evar_hyps (Global.env()) in
- Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
-
(* This exception is raised by *.existential_value *)
exception NotInstantiatedEvar
@@ -363,11 +354,86 @@ type evar_constraint = conv_pb * Environ.env * constr * constr
module EvMap = Evar.Map
+module EvNames :
+sig
+
+open Misctypes
+
+type t
+
+val empty : t
+val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val remove_name_defined : Evar.t -> t -> t
+val rename : Evar.t -> Id.t -> t -> t
+val reassign_name_defined : Evar.t -> Evar.t -> t -> t
+val ident : Evar.t -> t -> Id.t option
+val key : Id.t -> t -> Evar.t
+
+end =
+struct
+
+type t = Id.t EvMap.t * existential_key Idmap.t
+
+let empty = (EvMap.empty, Idmap.empty)
+
+let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
+ let id = match naming with
+ | Misctypes.IntroAnonymous -> None
+ | Misctypes.IntroIdentifier id ->
+ if Idmap.mem id idtoev then
+ user_err_loc
+ (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
+ Some id
+ | Misctypes.IntroFresh id ->
+ let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+ Some id
+ in
+ match id with
+ | None -> names
+ | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+
+let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
+ if EvMap.mem evk evtoid then
+ evar_names
+ else
+ add_name_newly_undefined naming evk evi evar_names
+
+let remove_name_defined evk (evtoid, idtoev as names) =
+ let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+ match id with
+ | None -> names
+ | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+
+let rename evk id (evtoid, idtoev) =
+ let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
+ match id' with
+ | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+ | Some id' ->
+ if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
+ (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+
+let reassign_name_defined evk evk' (evtoid, idtoev as names) =
+ let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+ match id with
+ | None -> names (** evk' must not be defined *)
+ | Some id ->
+ (EvMap.add evk' id (EvMap.remove evk evtoid),
+ Idmap.add id evk' (Idmap.remove id idtoev))
+
+let ident evk (evtoid, _) =
+ try Some (EvMap.find evk evtoid) with Not_found -> None
+
+let key id (_, idtoev) =
+ Idmap.find id idtoev
+
+end
+
type evar_map = {
(** Existential variables *)
defn_evars : evar_info EvMap.t;
undf_evars : evar_info EvMap.t;
- evar_names : Id.t EvMap.t * existential_key Idmap.t;
+ evar_names : EvNames.t;
(** Universes *)
universes : evar_universe_context;
(** Conversion problems *)
@@ -392,55 +458,15 @@ type evar_map = {
(*** Lifting primitive from Evar.Map. ***)
-let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
- let id = match naming with
- | Misctypes.IntroAnonymous ->
- let id = evar_ident_info evi in
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
- | Misctypes.IntroIdentifier id ->
- let id' =
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
- if not (Names.Id.equal id id') then
- user_err_loc
- (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
- id'
- | Misctypes.IntroFresh id ->
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
- (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
-
-let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
- if EvMap.mem evk evtoid then
- evar_names
- else
- add_name_newly_undefined naming evk evi evar_names
-
-let remove_name_defined evk (evtoid,idtoev) =
- let id = EvMap.find evk evtoid in
- (EvMap.remove evk evtoid, Idmap.remove id idtoev)
-
-let remove_name_possibly_already_defined evk evar_names =
- try remove_name_defined evk evar_names
- with Not_found -> evar_names
-
let rename evk id evd =
- let (evtoid,idtoev) = evd.evar_names in
- let id' = EvMap.find evk evtoid in
- if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
- { evd with evar_names =
- (EvMap.add evk id evtoid (* overwrite old name *),
- Idmap.add id evk (Idmap.remove id' idtoev)) }
-
-let reassign_name_defined evk evk' (evtoid,idtoev) =
- let id = EvMap.find evk evtoid in
- (EvMap.add evk' id (EvMap.remove evk evtoid),
- Idmap.add id evk' (Idmap.remove id idtoev))
+ { evd with evar_names = EvNames.rename evk id evd.evar_names }
let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
| Evar_empty ->
- let evar_names = add_name_undefined naming e i d.evar_names in
+ let evar_names = EvNames.add_name_undefined naming e i d.evar_names in
{ d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
| Evar_defined _ ->
- let evar_names = remove_name_possibly_already_defined e d.evar_names in
+ let evar_names = EvNames.remove_name_defined e d.evar_names in
{ d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
let add d e i = add_with_name d e i
@@ -583,7 +609,7 @@ let empty = {
last_mods = Evar.Set.empty;
metas = Metamap.empty;
effects = Safe_typing.empty_private_constants;
- evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
+ evar_names = EvNames.empty; (* id<->key for undefined evars *)
future_goals = [];
principal_future_goal = None;
extras = Store.empty;
@@ -619,14 +645,8 @@ let add_conv_pb ?(tail=false) pb d =
let evar_source evk d = (find d evk).evar_source
-let evar_ident evk evd =
- try EvMap.find evk (fst evd.evar_names)
- with Not_found ->
- (* Unnamed (non-dependent) evar *)
- add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
-
-let evar_key id evd =
- Idmap.find id (snd evd.evar_names)
+let evar_ident evk evd = EvNames.ident evk evd.evar_names
+let evar_key id evd = EvNames.key id evd.evar_names
let define_aux def undef evk body =
let oldinfo =
@@ -648,7 +668,7 @@ let define evk body evd =
| [] -> evd.last_mods
| _ -> Evar.Set.add evk evd.last_mods
in
- let evar_names = remove_name_defined evk evd.evar_names in
+ let evar_names = EvNames.remove_name_defined evk evd.evar_names in
{ evd with defn_evars; undf_evars; last_mods; evar_names }
let restrict evk filter ?candidates evd =
@@ -658,7 +678,7 @@ let restrict evk filter ?candidates evd =
{ evar_info with evar_filter = filter;
evar_candidates = candidates;
evar_extra = Store.empty } in
- let evar_names = reassign_name_defined evk evk' evd.evar_names in
+ let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
let ctxt = Filter.filter_list filter (evar_context evar_info) in
let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
let body = mkEvar(evk',id_inst) in
@@ -1196,7 +1216,34 @@ type unsolvability_explanation = SeveralInstancesFound of int
(**********************************************************)
(* Pretty-printing *)
-let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+let pr_evar_suggested_name evk sigma =
+ let base_id evk' evi =
+ match evar_ident evk' sigma with
+ | Some id -> id
+ | None -> match evi.evar_source with
+ | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+ | _,Evar_kinds.VarInstance id -> id
+ | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+ | _ ->
+ let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+ Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+ in
+ let names = EvMap.mapi base_id sigma.undf_evars in
+ let id = EvMap.find evk names in
+ let fold evk' id' (seen, n) =
+ if seen then (seen, n)
+ else if Evar.equal evk evk' then (true, n)
+ else if Id.equal id id' then (seen, succ n)
+ else (seen, n)
+ in
+ let (_, n) = EvMap.fold fold names (false, 0) in
+ if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk = match evar_ident evk sigma with
+| None ->
+ str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+ str "?" ++ pr_id id
let pr_instance_status (sc,typ) =
begin match sc with
@@ -1385,7 +1432,7 @@ let pr_evar_list sigma l =
h 0 (str (string_of_existential ev) ++
str "==" ++ pr_evar_info evi ++
(if evi.evar_body == Evar_empty
- then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
+ then str " {" ++ pr_existential_key sigma ev ++ str "}"
else mt ()))
in
h 0 (prlist_with_sep fnl pr l)
diff --git a/engine/evd.mli b/engine/evd.mli
index c8753b9c0..a9ca9a740 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -246,7 +246,7 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
(** Convenience function. Wrapper around {!find} to recover the source of an
evar in a given evar map. *)
-val evar_ident : existential_key -> evar_map -> Id.t
+val evar_ident : existential_key -> evar_map -> Id.t option
val rename : existential_key -> Id.t -> evar_map -> evar_map
@@ -597,6 +597,8 @@ type unsolvability_explanation = SeveralInstancesFound of int
val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
(** {5 Debug pretty-printers} *)
val pr_evar_info : evar_info -> Pp.std_ppcmds
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 70a35c613..9cdcb9e38 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -982,7 +982,10 @@ let rec glob_of_pat env sigma = function
| PEvar (evk,l) ->
let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
- let id = Evd.evar_ident evk sigma in
+ let id = match Evd.evar_ident evk sigma with
+ | None -> Id.of_string "__"
+ | Some id -> id
+ in
GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
diff --git a/lib/system.ml b/lib/system.ml
index 779e30816..13cfad4ae 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -199,10 +199,12 @@ let is_in_path lpath filename =
with Not_found -> false
let is_in_system_path filename =
- let path = try Sys.getenv "PATH"
- with Not_found -> error "system variable PATH not found" in
- let lpath = CUnix.path_to_list path in
- is_in_path lpath filename
+ try
+ let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
+ is_in_path lpath filename
+ with Not_found ->
+ msg_warning (str "system variable PATH not found");
+ false
let open_trapping_failure name =
try open_out_bin name
diff --git a/library/universes.ml b/library/universes.ml
index 68e422e00..c4eb2afcb 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -954,10 +954,10 @@ let universes_of_constr c =
let rec aux s c =
match kind_of_term c with
| Const (_, u) | Ind (_, u) | Construct (_, u) ->
- LSet.union (Instance.levels u) s
+ LSet.fold LSet.add (Instance.levels u) s
| Sort u when not (Sorts.is_small u) ->
let u = univ_of_sort u in
- LSet.union (Universe.levels u) s
+ LSet.fold LSet.add (Universe.levels u) s
| _ -> fold_constr aux s c
in aux LSet.empty c
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c8ecf91d3..b76409f43 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -517,7 +517,10 @@ let rec detype flags avoid env sigma t =
with Not_found -> isVarId id c in
let id,l =
try
- let id = Evd.evar_ident evk sigma in
+ let id = match Evd.evar_ident evk sigma with
+ | None -> Evd.pr_evar_suggested_name evk sigma
+ | Some id -> id
+ in
let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8c210e283..cd5188cd7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -351,14 +351,7 @@ let new_pure_evar_full evd evi =
(evd, evk)
let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
- let default_naming =
- if principal then
- (* waiting for a more principled approach
- (unnamed evars, private names?) *)
- Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
- else
- Misctypes.IntroAnonymous
- in
+ let default_naming = Misctypes.IntroAnonymous in
let naming = Option.default default_naming naming in
let evi = {
evar_hyps = sign;
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3d6196c35..fc8fab2f9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -494,15 +494,18 @@ let is_instance = function
let resolvable = Store.field ()
let set_resolvable s b =
- Store.set s resolvable b
+ if b then Store.remove s resolvable
+ else Store.set s resolvable ()
let is_resolvable evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
- Option.default true (Store.get evi.evar_extra resolvable)
+ Option.is_empty (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- let t = Store.set evi.evar_extra resolvable b in
- { evi with evar_extra = t }
+ if is_resolvable evi = b then evi
+ else
+ let t = set_resolvable evi.evar_extra b in
+ { evi with evar_extra = t }
let mark_resolvability b evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b5e882bc4..027a3f86c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1469,9 +1469,7 @@ let default_matching_core_flags sigma =
check_applied_meta_types = true;
use_pattern_unification = false;
use_meta_bound_pattern_unification = false;
- frozen_evars =
- fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
- sigma Evar.Set.empty;
+ frozen_evars = Evar.Map.domain (Evd.undefined_map sigma);
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = false;
diff --git a/printing/printer.ml b/printing/printer.ml
index 93850e41f..642098265 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -400,7 +400,7 @@ let display_name = false
(* display a goal name *)
let pr_goal_name sigma g =
- if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+ if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
else mt ()
(* display the conclusion of a goal *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1dd5be0e7..43a3024e5 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -89,7 +89,10 @@ module V82 = struct
(* Instantiates a goal with an open term, using name of goal for evk' *)
let partial_solution_to sigma evk evk' c =
let id = Evd.evar_ident evk sigma in
- Evd.rename evk' id (partial_solution sigma evk c)
+ let sigma = partial_solution sigma evk c in
+ match id with
+ | None -> sigma
+ | Some id -> Evd.rename evk' id sigma
(* Parts of the progress tactical *)
let same_goal evars1 gl1 evars2 gl2 =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ff8effcda..8008b0025 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1128,7 +1128,10 @@ struct
| None -> Evd.define gl.Goal.self c sigma
| Some evk ->
let id = Evd.evar_ident gl.Goal.self sigma in
- Evd.rename evk id (Evd.define gl.Goal.self c sigma)
+ let sigma = Evd.define gl.Goal.self c sigma in
+ match id with
+ | None -> sigma
+ | Some id -> Evd.rename evk id sigma
in
(** Restore the [future goals] state. *)
let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
diff --git a/stm/stm.ml b/stm/stm.ml
index e8b500a62..5bc0c5930 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -513,7 +513,10 @@ end = struct (* {{{ *)
let rec fill id =
if (get_info id).state = None then fill (Vcs_aux.visit v id).next
else copy_info_w_state v id in
- fill stop
+ let v = fill stop in
+ (* We put in the new dag the first state (since Qed shall run on it,
+ * see check_task_aux) *)
+ copy_info_w_state v start
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
@@ -1685,6 +1688,13 @@ let collect_proof keep cur hd brkind id =
| _ -> false in
let may_pierce_opaque = function
| { expr = VernacPrint (PrintName _) } -> true
+ (* These do not exactly pierce opaque, but are anyway impossible to properly
+ * delegate *)
+ | { expr = (VernacDeclareModule _
+ | VernacDefineModule _
+ | VernacDeclareModuleType _
+ | VernacInclude _) } -> true
+ | { expr = (VernacRequire _ | VernacImport _) } -> true
| _ -> false in
let parent = function Some (p, _) -> p | None -> assert false in
let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index ced6d9594..79671ce93 100644
--- a/test-suite/bugs/closed/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -56,7 +56,7 @@ Section Finite_nat_set.
subst fs1.
apply iff_refl.
intros H.
- eapply counted_list_equal_nth_char.
+ eapply (counted_list_equal_nth_char _ _ _ _ ?[def]).
intros i.
destruct (counted_def_nth fs1 i _ ) eqn:H0.
(* This was not part of the initial bug report; this is to check that
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed0..9680d2bbf 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
+Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
Existential 2 =
?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used)
Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b1558dab1..26eaca827 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
| NONE2 => 0
end
: option Z -> Z
-fun x : list ?T1 => match x with
- | NIL => NONE2
- | (_ :') t => SOME2 t
- end
- : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+ | NIL => NONE2
+ | (_ :') t => SOME2 t
+ end
+ : list ?T -> option (list ?T)
where
-?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1,
- x0 cannot be used)
+?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1,
+ x0 cannot be used)
s
: s
10
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c5a393408..576fbd7c0 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
fun n : nat => let x := A n : T n in ?y ?y0 : T n
: forall n : nat, T n
where
-?y : [n : nat x := A n : T n |- ?T0 -> T n]
-?y0 : [n : nat x := A n : T n |- ?T0]
+?y : [n : nat x := A n : T n |- ?T -> T n]
+?y0 : [n : nat x := A n : T n |- ?T]
fun n : nat => ?y ?y0 : T n
: forall n : nat, T n
where
-?y : [n : nat |- ?T0 -> T n]
-?y0 : [n : nat |- ?T0]
+?y : [n : nat |- ?T -> T n]
+?y0 : [n : nat |- ?T]
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 8fd039462..56ed89ed8 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -70,7 +70,7 @@ Abort.
Goal (forall x y : nat, x = y -> S x = S y) -> True.
intros.
-einjection (H O) as H0.
+einjection (H O ?[y]) as H0.
instantiate (y:=O).
Abort.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 55b666b72..02e043bc3 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -543,7 +543,7 @@ Qed.
Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
exists x, exists y, X x y.
Proof.
-intros; eexists; eexists; case H.
+intros; eexists; eexists ?[y]; case H.
apply (foo ?y).
Grab Existential Variables.
exact 0.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 9f091e399..90a60daa6 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -96,21 +96,21 @@ Abort.
(* Check that subterm selection does not solve existing evars *)
Goal exists x, S x = S 0.
-eexists.
+eexists ?[x].
Show x. (* Incidentally test Show on a named goal *)
destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
change (0 = S 0).
Abort.
Goal exists x, S 0 = S x.
-eexists.
+eexists ?[x].
destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
change (0 = S ?x).
[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
Abort.
Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
-do 2 eexists.
+eexists ?[n]; eexists ?[p].
destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
Abort.
@@ -426,7 +426,7 @@ destruct b eqn:H.
(* Check natural instantiation behavior when the goal has already an evar *)
Goal exists x, S x = x.
-eexists.
+eexists ?[x].
destruct (S _).
change (0 = ?x).
Abort.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4a5f14917..575e930ea 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1207,7 +1207,7 @@ let explain_unused_clause env pats =
let explain_non_exhaustive env pats =
str "Non exhaustive pattern-matching: no clause found for " ++
str (String.plural (List.length pats) "pattern") ++
- spc () ++ hov 0 (pr_sequence pr_cases_pattern pats)
+ spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
let explain_cannot_infer_predicate env sigma typs =
let env = make_all_name_different env in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 20:11:23 +0000