aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml5
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/evarutil.ml9
-rw-r--r--pretyping/evd.ml103
-rw-r--r--pretyping/evd.mli4
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/goal.ml5
-rw-r--r--proofs/proofview.ml5
-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/apply.v2
-rw-r--r--test-suite/success/destruct.v8
14 files changed, 102 insertions, 73 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9df8f9c233..cc5d189e04 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -988,7 +988,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/pretyping/detyping.ml b/pretyping/detyping.ml
index c3877c56e4..0c487ced81 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -518,7 +518,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 e23e5a53a7..759e0e4d6d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -365,14 +365,7 @@ let new_pure_evar_full evd evi =
(evd, evk)
let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?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 newevk = new_untyped_evar() in
let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 8be09a7821..0bc688aacf 100644
--- a/pretyping/evd.ml
+++ b/pretyping/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
@@ -588,7 +579,7 @@ val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> 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
+val ident : Evar.t -> t -> Id.t option
val key : Id.t -> t -> Evar.t
end =
@@ -598,21 +589,21 @@ 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) =
+let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
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.IntroAnonymous -> None
| 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'
+ 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 ->
- Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
- (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+ 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
@@ -620,25 +611,30 @@ let add_name_undefined naming evk evi (evtoid,idtoev as 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_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' = EvMap.find evk evtoid in
- if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
- (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))
+ 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 EvMap.find evk evtoid
- with Not_found ->
- (* Unnamed (non-dependent) evar *)
- add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
+ try Some (EvMap.find evk evtoid) with Not_found -> None
let key id (_, idtoev) =
Idmap.find id idtoev
@@ -682,7 +678,7 @@ let add d e i = match i.evar_body with
let evar_names = EvNames.add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
{ d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
| Evar_defined _ ->
- let evar_names = try EvNames.remove_name_defined e d.evar_names with Not_found -> 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 remove d e =
@@ -1706,7 +1702,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
@@ -1895,7 +1918,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/pretyping/evd.mli b/pretyping/evd.mli
index 9cfca02ed8..d2479c1229 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -249,7 +249,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
@@ -603,6 +603,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/printing/printer.ml b/printing/printer.ml
index 5ad0e45319..63755d7ff7 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 1dd5be0e71..43a3024e50 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 a6d9735f14..49228c93ac 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1093,7 +1093,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/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index ced6d95949..79671ce930 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 52e1e0ed01..9680d2bbff 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 b1558dab1c..26eaca8272 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 f2d1447785..4512e2c5ce 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 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/apply.v b/test-suite/success/apply.v
index 55b666b723..02e043bc36 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 9f091e3996..90a60daa66 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 20:59:26 +0000